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  2496  moor  2553  ssun1  4130  reuun1  4275  opthpr  4807  prel12g  4819  opthprneg  4820  disjord  5091  elelsuc  6388  ordssun  6417  fununmo  6545  tpres  7146  soxp  8053  poxp2  8067  poxp3  8074  omopth2  8523  swoord1  8637  swoord2  8638  nelaneq  9493  sornom  10171  fin56  10287  fpwwe2lem11  10535  ltle  11201  nn1m1nn  12132  elnnz  12467  elnn0z  12470  zmulcl  12510  nn01to3  12820  ltpnf  12995  xrltle  13022  xrltne  13036  swrdnnn0nd  14502  s3sndisj  14812  s3iunsndisj  14813  nn0o1gt2  16223  prm23lt5  16646  4sqlem17  16793  cshwsidrepswmod0  16927  cshwsdisj  16931  cshwshash  16937  funcres2c  17748  tsrlemax  18435  odlem1  19276  gexlem1  19320  drngmuleq0  20165  maducoeval2  21941  alexsubALTlem3  23352  dyadmbl  24916  gausslemma2dlem0f  26661  nb3grprlem1  28157  frgrwopreg  29096  frgrregorufr  29098  2wspmdisj  29110  frgrregord13  29169  satfvsucsuc  33771  dfon2lem4  34177  naddunif  34247  dfrdg4  34474  btwnconn1  34624  segcon2  34628  broutsideof2  34645  lineunray  34670  meran1  34821  dissym1  34831  bj-orim2  34957  bj-peircecurry  34959  bj-consensus  34980  bj-sbsb  35240  bj-unrab  35334  wl-orel12  35908  orfa  36479  tsor2  36545  lkrlspeqN  37571  sbor2  40567  omcl3g  41574  fzunt  41638  fzuntd  41639  fzunt1d  41640  fzuntgd  41641  ifpid1g  41677  ifpim3  41679  rp-fakeanorass  41696  or3or  42206  clsk1indlem3  42226  ntrclsk3  42253  19.33-2  42573  ax6e2ndeq  42752  uunT1  42973  undif3VD  43075  ax6e2ndeqVD  43102  ax6e2ndeqALT  43124  salexct  44476  salexct3  44484  salgencntex  44485  salgensscntex  44486  ndmafv2nrn  45355  otiunsndisjX  45412  prproropf1olem4  45599  poprelb  45617  nn0o1gt2ALTV  45787  odd2prm2  45811  ldepspr  46455  elfzolborelfzop1  46501  blen1b  46575  reorelicc  46697  eximp-surprise2  47133
  Copyright terms: Public domain W3C validator