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

Theorem orc 864
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 860 1 (𝜑 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 844
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 210  df-or 845
This theorem is referenced by:  pm1.4  866  orcd  870  orcs  872  pm2.45  879  norbi  884  pm2.67-2  889  pm2.4  904  pm1.5  917  biort  933  biorfi  936  pm4.72  947  pm3.48  961  pm4.44  994  pm4.45  995  orabs  996  pm5.61  998  andi  1005  pm5.71  1025  dedlema  1041  consensus  1048  ifptru  1071  3mix1  1327  norasslem2  1532  cad0  1619  cad11  1621  19.33  1885  19.33b  1886  dfsb2  2514  dfsb2ALT  2570  moor  2616  ssun1  4102  reuun1  4240  opthpr  4745  prel12g  4757  opthprneg  4758  disjord  5021  elelsuc  6235  ordssun  6262  fununmo  6375  tpres  6944  soxp  7810  omopth2  8197  swoord1  8307  swoord2  8308  nelaneq  9051  sornom  9692  fin56  9808  fpwwe2lem12  10056  ltle  10722  nn1m1nn  11650  elnnz  11983  elnn0z  11986  zmulcl  12023  nn01to3  12333  ltpnf  12507  xrltle  12534  xrltne  12548  swrdnnn0nd  14013  s3sndisj  14322  s3iunsndisj  14323  nn0o1gt2  15726  prm23lt5  16145  4sqlem17  16291  cshwsidrepswmod0  16424  cshwsdisj  16428  cshwshash  16434  funcres2c  17167  tsrlemax  17826  odlem1  18659  gexlem1  18700  drngmuleq0  19522  maducoeval2  21249  alexsubALTlem3  22658  dyadmbl  24208  gausslemma2dlem0f  25949  nb3grprlem1  27174  frgrwopreg  28112  frgrregorufr  28114  2wspmdisj  28126  frgrregord13  28185  satfvsucsuc  32726  dfon2lem4  33145  dfrdg4  33526  btwnconn1  33676  segcon2  33680  broutsideof2  33697  lineunray  33722  meran1  33873  dissym1  33883  bj-orim2  34005  bj-peircecurry  34007  bj-consensus  34025  bj-sbsb  34276  bj-unrab  34369  wl-orel12  34915  orfa  35519  tsor2  35585  lkrlspeqN  36466  sbor2  39388  ifpid1g  40195  ifpim3  40197  rp-fakeanorass  40214  or3or  40717  clsk1indlem3  40739  ntrclsk3  40766  19.33-2  41079  ax6e2ndeq  41258  uunT1  41479  undif3VD  41581  ax6e2ndeqVD  41608  ax6e2ndeqALT  41630  salexct  42967  salexct3  42975  salgencntex  42976  salgensscntex  42977  ndmafv2nrn  43771  otiunsndisjX  43828  prproropf1olem4  44016  poprelb  44034  nn0o1gt2ALTV  44205  odd2prm2  44229  ldepspr  44875  elfzolborelfzop1  44921  blen1b  44995  reorelicc  45117  eximp-surprise2  45306
  Copyright terms: Public domain W3C validator