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

Theorem orc 885
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 122 . 2 (𝜑 → (¬ 𝜑𝜓))
21orrd 881 1 (𝜑 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 865
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 198  df-or 866
This theorem is referenced by:  pm1.4  887  orcd  891  orcs  893  pm2.45  897  norbi  902  pm2.67-2  907  pm2.4  921  pm1.5  934  biort  950  biorfi  953  pm4.72  963  pm3.48  977  pm4.44  1010  pm4.45  1011  orabs  1012  andi  1021  pm5.71  1043  dedlema  1059  consensus  1068  ifptru  1089  3mix1  1422  cad0  1711  cad11  1713  19.33  1974  19.33b  1975  dfsb2  2531  moor  2687  ssun1  3969  reuun1  4104  opthpr  4564  prel12g  4579  opthprneg  4580  disjord  4826  elelsuc  6004  ordelinelOLD  6033  ordssun  6034  fununmo  6141  tpres  6685  soxp  7518  omopth2  7895  swoord1  8004  swoord2  8005  nelaneq  8737  sornom  9378  fin56  9494  fpwwe2lem12  9742  ltle  10405  nn1m1nn  11319  elnnz  11647  elnn0z  11650  zmulcl  11686  nn01to3  11994  ltpnf  12164  xrltle  12192  xrltne  12206  s3sndisj  13925  s3iunsndisj  13926  nn0o1gt2  15311  prm23lt5  15730  4sqlem17  15876  cshwsidrepswmod0  16007  cshwsdisj  16011  cshwshash  16017  funcres2c  16759  tsrlemax  17419  odlem1  18149  gexlem1  18189  drngmuleq0  18968  maducoeval2  20651  alexsubALTlem3  22060  dyadmbl  23575  bcmono  25210  gausslemma2dlem0f  25294  nb3grprlem1  26492  frgrwopreg  27492  frgrregorufr  27494  2wspmdisj  27506  frgrregord13  27578  dfon2lem4  32005  dfrdg4  32373  btwnconn1  32523  segcon2  32527  broutsideof2  32544  lineunray  32569  meran1  32721  dissym1  32731  bj-orim2  32851  bj-peircecurry  32855  bj-consensus  32871  bj-sbsb  33131  bj-unrab  33227  wl-orel12  33604  orfa  34186  tsor2  34259  lkrlspeqN  34945  fnwe2lem3  38117  ifpid1g  38333  ifpim3  38335  rp-fakeanorass  38352  or3or  38813  clsk1indlem3  38835  ntrclsk3  38862  19.33-2  39075  ax6e2ndeq  39267  uunT1  39498  undif3VD  39606  ax6e2ndeqVD  39633  ax6e2ndeqALT  39655  disjxp1  39725  salexct  41025  salexct3  41033  salgencntex  41034  salgensscntex  41035  ndmafv2nrn  41805  otiunsndisjX  41863  nn0o1gt2ALTV  42174  odd2prm2  42196  ldepspr  42824  elfzolborelfzop1  42871  blen1b  42944  eximp-surprise2  43096
  Copyright terms: Public domain W3C validator