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

Theorem orc 861
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 857 1 (𝜑 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 841
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 208  df-or 842
This theorem is referenced by:  pm1.4  863  orcd  869  orcs  871  pm2.45  875  norbi  880  pm2.67-2  885  pm2.4  900  pm1.5  913  biort  929  biorfi  932  pm4.72  943  pm3.48  957  pm4.44  990  pm4.45  991  orabs  992  pm5.61  994  andi  1001  pm5.71  1021  dedlema  1037  consensus  1044  ifptru  1065  3mix1  1322  norasslem2  1522  cad0  1609  cad11  1611  19.33  1876  19.33b  1877  dfsb2  2525  dfsb2ALT  2584  moor  2631  ssun1  4145  reuun1  4282  opthpr  4774  prel12g  4786  opthprneg  4787  disjord  5045  elelsuc  6256  ordssun  6283  fununmo  6394  tpres  6955  soxp  7812  omopth2  8199  swoord1  8309  swoord2  8310  nelaneq  9051  sornom  9687  fin56  9803  fpwwe2lem12  10051  ltle  10717  nn1m1nn  11646  elnnz  11979  elnn0z  11982  zmulcl  12019  nn01to3  12329  ltpnf  12503  xrltle  12530  xrltne  12544  swrdnnn0nd  14006  s3sndisj  14315  s3iunsndisj  14316  nn0o1gt2  15720  prm23lt5  16139  4sqlem17  16285  cshwsidrepswmod0  16416  cshwsdisj  16420  cshwshash  16426  funcres2c  17159  tsrlemax  17818  odlem1  18592  gexlem1  18633  drngmuleq0  19454  maducoeval2  21177  alexsubALTlem3  22585  dyadmbl  24128  gausslemma2dlem0f  25864  nb3grprlem1  27089  frgrwopreg  28029  frgrregorufr  28031  2wspmdisj  28043  frgrregord13  28102  satfvsucsuc  32509  dfon2lem4  32928  dfrdg4  33309  btwnconn1  33459  segcon2  33463  broutsideof2  33480  lineunray  33505  meran1  33656  dissym1  33666  bj-orim2  33788  bj-peircecurry  33790  bj-consensus  33808  bj-sbsb  34057  bj-unrab  34141  wl-orel12  34633  orfa  35241  tsor2  35307  lkrlspeqN  36187  sbor2  38982  ifpid1g  39738  ifpim3  39740  rp-fakeanorass  39757  or3or  40249  clsk1indlem3  40271  ntrclsk3  40298  19.33-2  40591  ax6e2ndeq  40770  uunT1  40991  undif3VD  41093  ax6e2ndeqVD  41120  ax6e2ndeqALT  41142  salexct  42494  salexct3  42502  salgencntex  42503  salgensscntex  42504  ndmafv2nrn  43298  otiunsndisjX  43355  prproropf1olem4  43545  poprelb  43563  nn0o1gt2ALTV  43736  odd2prm2  43760  ldepspr  44456  elfzolborelfzop1  44502  blen1b  44576  reorelicc  44625  eximp-surprise2  44814
  Copyright terms: Public domain W3C validator