MP
p→q, p ∴ q
MT
p→q, ~q ∴ ~p
DS
p∨q, ~p ∴ q (OR) p∨q, ~q ∴ p
Simp
p∙q ∴ p or q
Conj
p, q ∴ (p∙q)
HS
p→q, (q→r) ∴ (p→r)
Add
p ∴ p∨q (OR) p ∴ q∨p
CD
p∨q, p→r, q→s ∴ r∨s
DN
p :: ~~p
EX
(p∙q)→r :: p→(q→r)
Com
p∙q :: q∙p (OR) p∨q :: q∨p
Dist
p∙(q∨r) :: (p∙q)∨(p∙r)
Dist
p∨(q∙r):: (p∨q)∙(p∨r)
As
p∨(q∨r) :: (p∨q)∨r
As
p∙(q∙r) :: (p∙q)∙r
Re
p :: p∙p (OR) p ::p∨p
DeM
~(p∙q) :: ~p∨~q (OR) ~(p∨q) :: ~p∙~q
ME
p↔q :: (p→q)∙(q→p)
ME
p↔q :: (p∙q)∨(~p∙~q)
Cont
p→q :: ~q→~p
MI
p→q :: ~p∨q