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

Theorem pm2.21 547
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 545 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4
This theorem was proved from axioms:  ax-in2 545
This theorem is referenced by:  pm2.21d  549  pm2.24  551  pm2.24i  553  pm2.21i  574  pm2.52  581  jarl  583  mtt  609  orel2  644  imorri  667  pm2.42  693  pm2.18dc  749  simplimdc  756  peircedc  819  pm4.82  856  pm5.71dc  867  dedlemb  876  mo2n  1925  exmodc  1947  exmonim  1948  nrexrmo  2520  opthpr  3534  0neqopab  5492  0mnnnnn0  7990
  Copyright terms: Public domain W3C validator