ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm2.21 Unicode version

Theorem pm2.21 557
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
StepHypRef Expression
1 ax-in2 555 1  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-in2 555
This theorem is referenced by:  pm2.21d  559  pm2.24  561  pm2.24i  563  pm2.21i  585  pm2.52  592  jarl  594  mtt  620  orel2  655  imorri  678  pm2.42  704  pm2.18dc  761  simplimdc  768  peircedc  831  pm4.82  868  pm5.71dc  879  dedlemb  888  mo2n  1944  exmodc  1966  exmonim  1967  nrexrmo  2543  opthpr  3570  0neqopab  5577  0mnnnnn0  8270  flqeqceilz  9267
  Copyright terms: Public domain W3C validator