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

Theorem pm2.21 607
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 605 1 𝜑 → (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-in2 605
This theorem is referenced by:  pm2.21d  609  pm2.24  611  pm2.24i  613  pm2.21i  636  jarl  648  mtt  675  orel2  716  imorri  739  pm2.42  767  pm2.18dc  841  simplimdc  846  peircedc  900  pm4.82  935  pm5.71dc  946  dedlemb  955  mo2n  2034  exmodc  2056  exmonim  2057  nrexrmo  2673  opthpr  3735  0neqopab  5866  0mnnnnn0  9122  flqeqceilz  10217
  Copyright terms: Public domain W3C validator