Theorem pm2.21 580

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

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-in2 578

This theorem is referenced by:  pm2.21d  582  pm2.24  584  pm2.24i  586  pm2.21i  608  pm2.52  615  jarl  617  mtt  643  orel2  678  imorri  701  pm2.42  727  pm2.18dc  784  simplimdc  791  peircedc  854  pm4.82  892  pm5.71dc  903  dedlemb  912  mo2n  1971  exmodc  1993  exmonim  1994  nrexrmo  2575  opthpr  3584  0neqopab  5602  0mnnnnn0  8457  flqeqceilz  9470