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

Theorem pm2.21 582
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 580 1  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-in2 580
This theorem is referenced by:  pm2.21d  584  pm2.24  586  pm2.24i  588  pm2.21i  610  pm2.52  617  jarl  619  mtt  645  orel2  680  imorri  703  pm2.42  729  pm2.18dc  788  simplimdc  795  peircedc  858  pm4.82  896  pm5.71dc  907  dedlemb  916  mo2n  1976  exmodc  1998  exmonim  1999  nrexrmo  2583  opthpr  3611  0neqopab  5676  0mnnnnn0  8675  flqeqceilz  9690
  Copyright terms: Public domain W3C validator