Base.thm

This file was automatically generated by Deduce.
This file summarizes the theorems proved in the file:
	Base.pf

or_not: (all P:bool, Q:bool. (if ((P or Q) and not (P)) then Q))

ex_mid: (all b:bool. (b or not (b)))

or_sym: (all P:bool, Q:bool. (P or Q) = (Q or P))

and_sym: (all P:bool, Q:bool. (P and Q) = (Q and P))

eq_true: (all P:bool. (if P then P = true))

eq_false: (all P:bool. (if not (P) then P = false))

iff_equal: (all P:bool, Q:bool. (if ((if P then Q) and (if Q then P)) then P = Q))