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

Theorem orc 399
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 121 . 2 (𝜑 → (¬ 𝜑𝜓))
21orrd 392 1 (𝜑 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382
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 197  df-or 384
This theorem is referenced by:  pm1.4  400  orcd  406  orcs  408  pm2.45  411  pm2.67-2  416  biorfi  421  biorfiOLD  422  pm1.5  545  pm2.4  600  pm4.44  602  pm4.45  726  pm3.48  914  orabs  936  norbi  940  andi  947  pm4.72  956  biort  974  pm5.71  1015  dedlema  1032  consensus  1041  ifptru  1061  3mix1  1415  cad0  1705  cad11  1707  19.33  1961  19.33b  1962  dfsb2  2510  moor  2664  ssun1  3919  undif3OLD  4032  reuun1  4052  eqoreldifOLD  4370  opthpr  4528  prel12g  4544  opthprneg  4545  disjord  4793  elelsuc  5958  ordelinelOLD  5987  ordssun  5988  fununmo  6094  tpres  6630  soxp  7458  omopth2  7833  swoord1  7942  swoord2  7943  nelaneq  8669  sornom  9291  fin56  9407  fpwwe2lem12  9655  ltle  10318  nn1m1nn  11232  elnnz  11579  elnn0z  11582  zmulcl  11618  nn01to3  11974  ltpnf  12147  xrltle  12175  xrltne  12187  s3sndisj  13907  s3iunsndisj  13908  nn0o1gt2  15299  prm23lt5  15721  4sqlem17  15867  cshwsidrepswmod0  16003  cshwsdisj  16007  cshwshash  16013  funcres2c  16762  tsrlemax  17421  odlem1  18154  gexlem1  18194  drngmuleq0  18972  maducoeval2  20648  alexsubALTlem3  22054  dyadmbl  23568  bcmono  25201  gausslemma2dlem0f  25285  nb3grprlem1  26480  frgrwopreg  27477  frgrregorufr  27479  2wspmdisj  27491  frgrregord13  27564  dfon2lem4  31996  dfrdg4  32364  btwnconn1  32514  segcon2  32518  broutsideof2  32535  lineunray  32560  meran1  32716  dissym1  32726  bj-orim2  32847  bj-peircecurry  32851  bj-consensus  32868  bj-sbsb  33130  bj-unrab  33228  wl-orel12  33607  orfa  34194  tsor2  34268  lkrlspeqN  34961  fnwe2lem3  38124  ifpid1g  38341  ifpim3  38343  rp-fakeanorass  38360  or3or  38821  clsk1indlem3  38843  ntrclsk3  38870  19.33-2  39083  ax6e2ndeq  39277  uunT1  39509  undif3VD  39617  ax6e2ndeqVD  39644  ax6e2ndeqALT  39666  disjxp1  39737  salexct  41055  salexct3  41063  salgencntex  41064  salgensscntex  41065  otiunsndisjX  41806  nn0o1gt2ALTV  42115  odd2prm2  42137  ldepspr  42772  elfzolborelfzop1  42819  blen1b  42892  eximp-surprise2  43044
  Copyright terms: Public domain W3C validator