Logica Tools
for
Thought
 
Hilbert
Copy Load Save Library
Objects  a, b, c
Functions  f, g

1 p => q Premise 2 (q => r) => (p => (q => r)) Implication Creation Schema 3 (p => (q => r)) => ((p => q) => (p => r)) Implication Distribution Schema 4 (q => r) => ((p => q) => (p => r)) Transitivity 2 3 5 (p => q) => ((q => r) => (p => q)) Implication Creation Schema 6 (q => r) => (p => q) Implication Elimination 5 1 7 (q => r) => (p => r) Conditional Deduction 4 6