Theorem orc 868

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 124	. 2 ⊢ (𝜑 → (¬ 𝜑 → 𝜓))
2	1	orrd 864	1 ⊢ (𝜑 → (𝜑 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 848

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 207  df-or 849

This theorem is referenced by:  pm1.4  870  orcd  874  orcs  876  pm2.45  882  norbi  887  pm2.67-2  892  pm2.4  907  pm1.5  920  biort  936  biorfriOLD  941  pm4.72  952  pm3.48  966  pm4.44  999  pm4.45  1000  orabs  1001  pm5.61  1003  andi  1010  pm5.71  1030  dedlema  1046  consensus  1053  ifptru  1075  3mix1  1332  cad11  1618  19.33  1886  19.33b  1887  dfsb2  2497  moor  2554  ssun1  4118  reuun1  4268  opthpr  4794  prel12g  4807  opthprneg  4808  disjord  5074  el  5390  elelsuc  6398  ordssun  6427  fununmo  6545  tpres  7156  fvf1pr  7262  soxp  8079  poxp2  8093  poxp3  8100  omopth2  8519  naddunif  8629  swoord1  8676  swoord2  8677  nelaneqOLDOLD  9518  sornom  10199  fin56  10315  fpwwe2lem11  10564  ltle  11234  nn1m1nn  12195  elnnz  12534  elnn0z  12537  zmulcl  12576  nn01to3  12891  ltpnf  13071  xrltle  13100  xrltne  13114  swrdnnn0nd  14619  s3sndisj  14929  s3iunsndisj  14930  nn0o1gt2  16350  prm23lt5  16785  4sqlem17  16932  cshwsidrepswmod0  17065  cshwsdisj  17069  cshwshash  17075  funcres2c  17870  tsrlemax  18552  odlem1  19510  gexlem1  19554  drngmuleq0  20740  maducoeval2  22605  alexsubALTlem3  24014  dyadmbl  25567  gausslemma2dlem0f  27324  eln0s  28353  elnnzs  28393  bdayfinbndlem2  28460  nb3grprlem1  29449  frgrwopreg  30393  frgrregorufr  30395  2wspmdisj  30407  frgrregord13  30466  satfvsucsuc  35547  dfon2lem4  35966  dfrdg4  36133  btwnconn1  36283  segcon2  36287  broutsideof2  36304  lineunray  36329  meran1  36593  dissym1  36603  weiunpo  36647  axtco1from2  36657  bj-orim2  36820  bj-peircecurry  36822  bj-consensus  36843  bj-sbsb  37144  bj-unrab  37233  bj-axseprep  37381  wl-orel12  37836  orfa  38403  tsor2  38469  lkrlspeqN  39617  sbor2  42651  omcl3g  43762  fzunt  43882  fzuntd  43883  fzunt1d  43884  fzuntgd  43885  ifpid1g  43921  ifpim3  43923  rp-fakeanorass  43940  or3or  44450  clsk1indlem3  44470  ntrclsk3  44497  19.33-2  44809  ax6e2ndeq  44986  uunT1  45206  undif3VD  45308  ax6e2ndeqVD  45335  ax6e2ndeqALT  45357  salexct  46762  salexct3  46770  salgencntex  46771  salgensscntex  46772  ndmafv2nrn  47670  otiunsndisjX  47727  prproropf1olem4  47966  poprelb  47984  nn0o1gt2ALTV  48170  odd2prm2  48194  clnbgrel  48304  dfclnbgr6  48332  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx13starlem2  48548  gpg5edgnedg  48606  ldepspr  48949  elfzolborelfzop1  48995  blen1b  49064  reorelicc  49186  opth1neg  49301  eximp-surprise2  50260