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 ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4

This proof depends on axioms:  ax-in2 624

This theorem is used 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  3897  0neqopab  6133  0mnnnnn0  9595  flqeqceilz  10755