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 120 . 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 196  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  597  pm4.44  599  pm4.45  720  pm3.48  874  orabs  896  norbi  900  andi  907  pm4.72  916  biort  936  pm5.71  973  consensus  990  dedlema  993  ifptru  1017  3mix1  1223  cad0  1547  cad11  1549  19.33  1801  19.33b  1802  dfsb2  2361  moor  2514  ssun1  3738  undif3OLD  3848  reuun1  3868  eqoreldifOLD  4173  opthpr  4324  elelsuc  5714  ordelinelOLD  5743  ordssun  5744  fununmo  5847  tpres  6371  soxp  7177  omopth2  7551  swoord1  7660  swoord2  7661  sornom  8982  fin56  9098  fpwwe2lem12  9342  ltle  10005  nn1m1nn  10917  elnnz  11264  elnn0z  11267  zmulcl  11303  nn01to3  11657  ltpnf  11830  xrltle  11858  xrltne  11870  s3sndisj  13554  s3iunsndisj  13555  nn0o1gt2  14935  prm23lt5  15357  4sqlem17  15503  cshwsidrepswmod0  15639  cshwsdisj  15643  cshwshash  15649  funcres2c  16384  tsrlemax  17043  odlem1  17777  gexlem1  17817  drngmuleq0  18593  maducoeval2  20265  alexsubALTlem3  21663  dyadmbl  23174  bcmono  24802  gausslemma2dlem0f  24886  nb3graprlem1  25980  frgrawopreg  26576  frgraregorufr  26580  2spotdisj  26588  2spotiundisj  26589  2spotmdisj  26595  frgraregord13  26646  dfon2lem4  30935  sltsgn1  31058  sltsgn2  31059  dfrdg4  31228  btwnconn1  31378  segcon2  31382  broutsideof2  31399  lineunray  31424  meran1  31580  dissym1  31590  bj-orim2  31711  bj-peircecurry  31715  bj-consensus  31732  bj-sbsb  32012  bj-unrab  32114  wl-orel12  32473  orfa  33051  tsor2  33125  lkrlspeqN  33476  fnwe2lem3  36640  ifpid1g  36858  ifpim3  36860  rp-fakeanorass  36877  or3or  37339  clsk1indlem3  37361  ntrclsk3  37388  19.33-2  37603  ax6e2ndeq  37796  uunT1  38028  undif3VD  38140  ax6e2ndeqVD  38167  ax6e2ndeqALT  38189  disjxp1  38263  nelpr1  38289  salexct  39228  salexct3  39236  salgencntex  39237  salgensscntex  39238  nn0o1gt2ALTV  40143  otiunsndisjX  40317  nb3grprlem1  40608  2wspdisj  41165  2wspiundisj  41166  frgrwopreg  41486  frgrregorufr  41490  2wspmdisj  41501  av-frgraregord13  41550  ldepspr  42056  elfzolborelfzop1  42103  blen1b  42180  eximp-surprise2  42340
  Copyright terms: Public domain W3C validator