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

Theorem pm2.21 529
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 φ → (φψ))

Proof of Theorem pm2.21
StepHypRef Expression
1 ax-in2 527 1 φ → (φψ))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4
This theorem is referenced by:  pm2.21d  531  pm2.24  532  pm2.24i  534  pm2.21i  553  pm2.52  560  jarl  562  mtt  588  orel2  620  imorri  643  pm2.42  669  pm2.18  722  pm2.18dc  723  notnot2  725  simplim  735  simplimdc  736  pm4.82  835  pm5.71  840  mo  1782  mo2  1789  exmo  1806  2mo  1839  ax11indi  1923
This theorem was proved from axioms:  ax-in2 527
  Copyright terms: Public domain W3C validator