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  2054  exmodc  2076  exmonim  2077  nrexrmo  2693  opthpr  3771  0neqopab  5915  0mnnnnn0  9202  flqeqceilz  10311