Theorem pm2.21 579

Description: From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. (Contributed by Mario Carneiro, 12-May-2015.)

Assertion

Ref	Expression
pm2.21	|- ( -. ph -> ( ph -> ps ) )

Proof of Theorem pm2.21

Step	Hyp	Ref	Expression
1		ax-in2 577	1 |- ( -. ph -> ( ph -> ps ) )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-in2 577

This theorem is referenced by:  pm2.21d  581  pm2.24  583  pm2.24i  585  pm2.21i  607  pm2.52  614  jarl  616  mtt  642  orel2  677  imorri  700  pm2.42  726  pm2.18dc  783  simplimdc  790  peircedc  853  pm4.82  891  pm5.71dc  902  dedlemb  911  mo2n  1969  exmodc  1991  exmonim  1992  nrexrmo  2570  opthpr  3564  0neqopab  5570  0mnnnnn0  8320  flqeqceilz  9320