MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orc Structured version   Visualization version   GIF version

Theorem orc 865
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 124 . 2 (𝜑 → (¬ 𝜑𝜓))
21orrd 861 1 (𝜑 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 845
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 206  df-or 846
This theorem is referenced by:  pm1.4  867  orcd  871  orcs  873  pm2.45  880  norbi  885  pm2.67-2  890  pm2.4  905  pm1.5  918  biort  934  biorfi  937  pm4.72  948  pm3.48  962  pm4.44  995  pm4.45  996  orabs  997  pm5.61  999  andi  1006  pm5.71  1026  dedlema  1044  consensus  1051  ifptru  1074  3mix1  1330  norasslem2  1536  cad11  1617  cad0OLD  1620  19.33  1887  19.33b  1888  dfsb2  2495  moor  2552  ssun1  4130  reuun1  4275  opthpr  4807  prel12g  4819  opthprneg  4820  disjord  5091  elelsuc  6388  ordssun  6417  fununmo  6545  tpres  7146  soxp  8057  poxp2  8071  poxp3  8078  omopth2  8527  naddunif  8633  swoord1  8675  swoord2  8676  nelaneq  9531  sornom  10209  fin56  10325  fpwwe2lem11  10573  ltle  11239  nn1m1nn  12170  elnnz  12505  elnn0z  12508  zmulcl  12548  nn01to3  12858  ltpnf  13033  xrltle  13060  xrltne  13074  swrdnnn0nd  14536  s3sndisj  14844  s3iunsndisj  14845  nn0o1gt2  16255  prm23lt5  16678  4sqlem17  16825  cshwsidrepswmod0  16959  cshwsdisj  16963  cshwshash  16969  funcres2c  17780  tsrlemax  18467  odlem1  19308  gexlem1  19352  drngmuleq0  20197  maducoeval2  21973  alexsubALTlem3  23384  dyadmbl  24948  gausslemma2dlem0f  26693  nb3grprlem1  28214  frgrwopreg  29153  frgrregorufr  29155  2wspmdisj  29167  frgrregord13  29226  satfvsucsuc  33828  dfon2lem4  34231  dfrdg4  34503  btwnconn1  34653  segcon2  34657  broutsideof2  34674  lineunray  34699  meran1  34850  dissym1  34860  bj-orim2  34986  bj-peircecurry  34988  bj-consensus  35009  bj-sbsb  35269  bj-unrab  35363  wl-orel12  35937  orfa  36508  tsor2  36574  lkrlspeqN  37600  sbor2  40596  omcl3g  41605  fzunt  41669  fzuntd  41670  fzunt1d  41671  fzuntgd  41672  ifpid1g  41708  ifpim3  41710  rp-fakeanorass  41727  or3or  42237  clsk1indlem3  42257  ntrclsk3  42284  19.33-2  42604  ax6e2ndeq  42783  uunT1  43004  undif3VD  43106  ax6e2ndeqVD  43133  ax6e2ndeqALT  43155  salexct  44507  salexct3  44515  salgencntex  44516  salgensscntex  44517  ndmafv2nrn  45386  otiunsndisjX  45443  prproropf1olem4  45630  poprelb  45648  nn0o1gt2ALTV  45818  odd2prm2  45842  ldepspr  46486  elfzolborelfzop1  46532  blen1b  46606  reorelicc  46728  eximp-surprise2  47164
  Copyright terms: Public domain W3C validator