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

Theorem orc 400
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 393 1 (𝜑 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 383
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 385
This theorem is referenced by:  pm1.4  401  orcd  407  orcs  409  pm2.45  412  pm2.67-2  417  biorfi  422  biorfiOLD  423  pm1.5  544  pm2.4  598  pm4.44  600  pm4.45  723  pm3.48  877  orabs  899  norbi  903  andi  910  pm4.72  919  biort  937  pm5.71  976  consensus  998  dedlema  1001  ifptru  1022  3mix1  1228  cad0  1553  cad11  1555  19.33  1809  19.33b  1810  dfsb2  2372  moor  2525  ssun1  3760  undif3OLD  3871  reuun1  3891  eqoreldifOLD  4204  opthpr  4359  elelsuc  5766  ordelinelOLD  5795  ordssun  5796  fununmo  5901  tpres  6431  soxp  7250  omopth2  7624  swoord1  7733  swoord2  7734  sornom  9059  fin56  9175  fpwwe2lem12  9423  ltle  10086  nn1m1nn  11000  elnnz  11347  elnn0z  11350  zmulcl  11386  nn01to3  11741  ltpnf  11914  xrltle  11942  xrltne  11954  s3sndisj  13656  s3iunsndisj  13657  nn0o1gt2  15040  prm23lt5  15462  4sqlem17  15608  cshwsidrepswmod0  15744  cshwsdisj  15748  cshwshash  15754  funcres2c  16501  tsrlemax  17160  odlem1  17894  gexlem1  17934  drngmuleq0  18710  maducoeval2  20386  alexsubALTlem3  21793  dyadmbl  23308  bcmono  24936  gausslemma2dlem0f  25020  nb3grprlem1  26203  2wspdisj  26757  2wspiundisj  26758  frgrwopreg  27078  frgrregorufr  27082  2wspmdisj  27093  frgrregord13  27142  dfon2lem4  31445  sltsgn1  31568  sltsgn2  31569  dfrdg4  31753  btwnconn1  31903  segcon2  31907  broutsideof2  31924  lineunray  31949  meran1  32105  dissym1  32115  bj-orim2  32236  bj-peircecurry  32240  bj-consensus  32257  bj-sbsb  32520  bj-unrab  32622  wl-orel12  32965  orfa  33552  tsor2  33626  lkrlspeqN  33977  fnwe2lem3  37141  ifpid1g  37359  ifpim3  37361  rp-fakeanorass  37378  or3or  37840  clsk1indlem3  37862  ntrclsk3  37889  19.33-2  38102  ax6e2ndeq  38296  uunT1  38528  undif3VD  38640  ax6e2ndeqVD  38667  ax6e2ndeqALT  38689  disjxp1  38760  salexct  39889  salexct3  39897  salgencntex  39898  salgensscntex  39899  otiunsndisjX  40625  nn0o1gt2ALTV  40934  ldepspr  41580  elfzolborelfzop1  41627  blen1b  41704  eximp-surprise2  41864
  Copyright terms: Public domain W3C validator