Logica ToolsforThought
 Fitch Proofs

 Name Description Depth Negation Introduction {p} ⊢ ~~p 0 Negation Elimination {~~p} ⊢ p 0 And Introduction {p, q} ⊢ p&q 0 And Elimination {p&q} ⊢ {p, q} 0 Or Introduction {p} ⊢ {p|q, q|p} 0 Or Elimination {p|q, p=>r, q=>r} ⊢ r 0 Implication Elimination {p=>q, p} ⊢ q 0 Biconditional Introduction {p=>q, q=>p} ⊢ p<=>q 0 Biconditional Elimination {p<=>q} ⊢ {p=>q, q=>p} 0 Implication Creation {p} ⊢ q=>p 1 Implication Distribution {p=>(q=>r)} ⊢ (p=>q)=>(p=r) 1 Implication Reversal {~q=>~p} ⊢ p=>q 1 Inconsistency {p, ~p} ⊢ q 1 Conditional Deduction {p=>(q=>r), p=>q} ⊢ p=>r 1 Transitivity {p=>q, q=>r} ⊢ p=>r 1 Condition Introduction {q=>r} ⊢ (p=>q)=>(p=>r) 1 Conclusion Introduction {p=>q} ⊢ (q=>r)=>(p=>r) 1 Condition Reversal {p=>(q=>r)} ⊢ q=>(p=>r) 1 Modus Tollens {p=>q, ~q} ⊢ ~p 1 Implication Reduction {p=>~p} ⊢ ~p 1 Contradiction Realization {p=>q, p=>~q} ⊢ ~p 1 Universal Conjunction {AX:(p(X)&q(X))} ⊢ AX:p(X)&AX:q(X) 1 Universal Implication {AX:(p(X)=>q(X))} ⊢ AX:p(X)=>AX:q(X) 1 Universal Reversal {AX:AY:p(X,Y)} ⊢ AY:AX:p(X,Y) 1 Existential Universal {EY:AX:p(X,Y)} ⊢ AX:EY:p(X,Y) 1