Theorem pm2.21 547

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

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-in2 545

This theorem is referenced by:  pm2.21d  549  pm2.24  551  pm2.24i  553  pm2.21i  575  pm2.52  582  jarl  584  mtt  610  orel2  645  imorri  668  pm2.42  694  pm2.18dc  750  simplimdc  757  peircedc  820  pm4.82  857  pm5.71dc  868  dedlemb  877  mo2n  1928  exmodc  1950  exmonim  1951  nrexrmo  2526  opthpr  3543  0neqopab  5550  0mnnnnn0  8214  flqeqceilz  9160