Theorem orc 880

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

Step	Hyp	Ref	Expression
1		pm2.24 125	. 2 ⊢ (𝜑 → (¬ 𝜑 → 𝜓))
2	1	orrd 876	1 ⊢ (𝜑 → (𝜑 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  pm1.4  882  orcd  886  orcs  888  pm2.45  894  norbi  899  pm2.67-2  904  pm2.4  919  pm1.5  932  biort  948  biorfriOLD  953  pm4.72  964  pm3.48  978  pm4.44  1012  pm4.45  1013  orabs  1014  pm5.61  1016  andi  1023  pm5.71  1043  dedlema  1059  consensus  1066  ifptru  1089  3mix1  1347  cad11  1639  19.33  1907  19.33b  1908  dfsb2  2527  moor  2584  ssun1  4133  reuun1  4283  opthpr  4812  prel12g  4825  opthprneg  4826  disjord  5094  el  5410  elelsuc  6425  ordssun  6454  fununmo  6572  tpres  7189  fvf1pr  7295  soxp  8113  poxp2  8127  poxp3  8134  omopth2  8557  naddunif  8668  swoord1  8715  swoord2  8716  nelaneqOLDOLD  9554  sornom  10249  fin56  10365  fpwwe2lem11  10614  ltle  11286  nn1m1nn  12245  elnnz  12592  elnn0z  12595  zmulcl  12634  nn01to3  12956  ltpnf  13136  xrltle  13165  xrltne  13179  swrdnnn0nd  14684  s3sndisj  14994  s3iunsndisj  14995  nn0o1gt2  16429  prm23lt5  16864  4sqlem17  17011  cshwsidrepswmod0  17144  cshwsdisj  17148  cshwshash  17154  funcres2c  17950  tsrlemax  18632  odlem1  19596  gexlem1  19640  drngmuleq0  20836  maducoeval2  22758  alexsubALTlem3  24167  dyadmbl  25720  gausslemma2dlem0f  27483  eln0s  28512  elnnzs  28552  bdayfinbndlem2  28619  nb3grprlem1  29639  frgrwopreg  30583  frgrregorufr  30585  2wspmdisj  30597  frgrregord13  30656  satfvsucsuc  35728  dfon2lem4  36147  dfrdg4  36314  btwnconn1  36464  segcon2  36468  broutsideof2  36485  lineunray  36510  meran1  36784  dissym1  36794  weiunpo  36838  axtco1from2  36848  bj-orim2  37010  bj-peircecurry  37012  bj-consensus  37033  bj-sbsb  37334  bj-unrab  37423  bj-axseprep  37571  wl-orel12  38026  orfa  38593  tsor2  38659  lkrlspeqN  39807  sbor2  42841  omcl3g  43923  fzunt  44043  fzuntd  44044  fzunt1d  44045  fzuntgd  44046  ifpid1g  44082  ifpim3  44084  rp-fakeanorass  44101  or3or  44611  clsk1indlem3  44631  ntrclsk3  44658  19.33-2  44956  ax6e2ndeq  45133  uunT1  45353  undif3VD  45455  ax6e2ndeqVD  45482  ax6e2ndeqALT  45504  salexct  46906  salexct3  46914  salgencntex  46915  salgensscntex  46916  ndmafv2nrn  47814  otiunsndisjX  47871  prproropf1olem4  48110  poprelb  48128  nn0o1gt2ALTV  48314  odd2prm2  48338  clnbgrel  48448  dfclnbgr6  48476  gpg5nbgrvtx03starlem2  48689  gpg5nbgrvtx13starlem2  48692  gpg5edgnedg  48750  ldepspr  49104  elfzolborelfzop1  49150  blen1b  49219  reorelicc  49341  opth1neg  49455  eximp-surprise2  50414