NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  orc Unicode version

Theorem orc 374
Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
orc

Proof of Theorem orc
StepHypRef Expression
1 pm2.24 101 . 2
21orrd 367 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wo 357
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177  df-or 359
This theorem is referenced by:  pm1.4  375  orcd  381  orcs  383  pm2.45  386  pm2.67-2  391  biorfi  396  pm1.5  508  pm2.4  558  pm4.44  560  pm4.45  669  pm3.48  806  orabs  828  andi  837  pm4.72  846  biort  866  pm5.71  902  dedlema  920  consensus  925  3mix1  1124  cad1  1398  cad11  1399  cad0  1400  19.33  1607  19.33b  1608  dfsb2  2055  moor  2257  ssun1  3426  undif3  3515  reuun1  3537  phiall  4618  clos1basesuc  5882  leconnnc  6218  ncslesuc  6267  nchoicelem9  6297
  Copyright terms: Public domain W3C validator