Theorem pm2.21 557

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 555	1 |- ( -. ph -> ( ph -> ps ) )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-in2 555

This theorem is referenced by:  pm2.21d  559  pm2.24  561  pm2.24i  563  pm2.21i  585  pm2.52  592  jarl  594  mtt  620  orel2  655  imorri  678  pm2.42  704  pm2.18dc  761  simplimdc  768  peircedc  831  pm4.82  868  pm5.71dc  879  dedlemb  888  mo2n  1944  exmodc  1966  exmonim  1967  nrexrmo  2543  opthpr  3570  0neqopab  5577  0mnnnnn0  8270  flqeqceilz  9267