Theorem pm2.21 626

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

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-in2 624

This theorem is referenced by:  pm2.21d  628  pm2.24  630  pm2.24i  632  pm2.21i  655  jarl  668  mtt  696  orel2  738  imorri  761  pm2.42  789  pm2.18dc  867  simplimdc  872  peircedc  926  pm4.82  963  pm5.71dc  974  dedlemb  983  mo2n  2114  exmodc  2137  exmonim  2138  nrexrmo  2774  opthpr  3892  0neqopab  6123  0mnnnnn0  9574  flqeqceilz  10733