▶ Here you can easily type logic and mathematics formulas and use them anywhere.

Examples:

forall S forsome P forall x(x elem P <=> x psubset S)	➟	∀S ∃P ∀x(x∈P⇔x⊂S)
[](p-)q)-)<>(p-)q)	➟	◻(p⊃q)⊃◇(p⊃q)
IPC |/- phi \/ --phi	➟	IPC⊬𝜙∨¬𝜙
--phi =- phi -> _|	➟	¬𝜙≡𝜙→⊥
Gamma |= phi => Gamma |- phi	➟	Γ⊨𝜙⇒Γ⊢𝜙

▶ You can check whether the entered formula(s) make a valid inference by clicking the Evaluate button.