Pithos ND
Application
GitHub
¬
∧
∨
→
↔
∀
∃
⊤
⊥
(
)
[
]
Givens
No givens specified.
Add given
Remove last given
Goal
The result of the parsing will appear here.
Start proof
∧I
∧E
∨I
∨E
→I
→E
¬I
¬E
¬¬E
⊤I
⊥I
⊥E
↔I
↔E
EM
PC
∃I
∃E
∀I
∀E
∀→I
∀→E
=sub
refl
=sym
✓
↶
↷
Proof
Modify input
Confirmation required
×
Do you really wish to discard your proof and modify the givens or the goal?