Theorem pm2.21 622

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

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-in2 620

This theorem is referenced by:  pm2.21d  624  pm2.24  626  pm2.24i  628  pm2.21i  651  jarl  664  mtt  691  orel2  733  imorri  756  pm2.42  784  pm2.18dc  862  simplimdc  867  peircedc  921  pm4.82  958  pm5.71dc  969  dedlemb  978  mo2n  2107  exmodc  2130  exmonim  2131  nrexrmo  2755  opthpr  3855  0neqopab  6065  0mnnnnn0  9433  flqeqceilz  10579