Theorem pm2.21 617

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

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-in2 615

This theorem is referenced by:  pm2.21d  619  pm2.24  621  pm2.24i  623  pm2.21i  646  jarl  658  mtt  685  orel2  726  imorri  749  pm2.42  777  pm2.18dc  855  simplimdc  860  peircedc  914  pm4.82  950  pm5.71dc  961  dedlemb  970  mo2n  2052  exmodc  2074  exmonim  2075  nrexrmo  2691  opthpr  3768  0neqopab  5910  0mnnnnn0  9181  flqeqceilz  10288