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  543  pm2.4  598  pm4.44  600  pm4.45  724  pm3.48  896  orabs  918  norbi  922  andi  929  pm4.72  938  biort  956  pm5.71  997  dedlema  1014  consensus  1023  ifptru  1043  3mix1  1250  cad0  1596  cad11  1598  19.33  1852  19.33b  1853  dfsb2  2401  moor  2555  ssun1  3809  undif3OLD  3922  reuun1  3942  eqoreldifOLD  4258  opthpr  4415  disjord  4673  elelsuc  5835  ordelinelOLD  5864  ordssun  5865  fununmo  5971  tpres  6507  soxp  7335  omopth2  7709  swoord1  7818  swoord2  7819  sornom  9137  fin56  9253  fpwwe2lem12  9501  ltle  10164  nn1m1nn  11078  elnnz  11425  elnn0z  11428  zmulcl  11464  nn01to3  11819  ltpnf  11992  xrltle  12020  xrltne  12032  s3sndisj  13752  s3iunsndisj  13753  nn0o1gt2  15144  prm23lt5  15566  4sqlem17  15712  cshwsidrepswmod0  15848  cshwsdisj  15852  cshwshash  15858  funcres2c  16608  tsrlemax  17267  odlem1  18000  gexlem1  18040  drngmuleq0  18818  maducoeval2  20494  alexsubALTlem3  21900  dyadmbl  23414  bcmono  25047  gausslemma2dlem0f  25131  nb3grprlem1  26326  frgrwopreg  27303  frgrregorufr  27305  2wspmdisj  27317  frgrregord13  27383  dfon2lem4  31815  dfrdg4  32183  btwnconn1  32333  segcon2  32337  broutsideof2  32354  lineunray  32379  meran1  32535  dissym1  32545  bj-orim2  32666  bj-peircecurry  32670  bj-consensus  32687  bj-sbsb  32949  bj-unrab  33047  wl-orel12  33424  orfa  34011  tsor2  34085  lkrlspeqN  34776  fnwe2lem3  37939  ifpid1g  38156  ifpim3  38158  rp-fakeanorass  38175  or3or  38636  clsk1indlem3  38658  ntrclsk3  38685  19.33-2  38898  ax6e2ndeq  39092  uunT1  39324  undif3VD  39432  ax6e2ndeqVD  39459  ax6e2ndeqALT  39481  disjxp1  39552  salexct  40870  salexct3  40878  salgencntex  40879  salgensscntex  40880  otiunsndisjX  41621  nn0o1gt2ALTV  41930  odd2prm2  41952  ldepspr  42587  elfzolborelfzop1  42634  blen1b  42707  eximp-surprise2  42859
  Copyright terms: Public domain W3C validator