Theorem pm2.21 606

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

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-in2 604

This theorem is referenced by:  pm2.21d  608  pm2.24  610  pm2.24i  612  pm2.21i  635  jarl  647  mtt  674  orel2  715  imorri  738  pm2.42  766  pm2.18dc  840  simplimdc  845  peircedc  899  pm4.82  934  pm5.71dc  945  dedlemb  954  mo2n  2027  exmodc  2049  exmonim  2050  nrexrmo  2647  opthpr  3699  0neqopab  5816  0mnnnnn0  9009  flqeqceilz  10091