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  1025  pm5.71  1045  dedlema  1061  consensus  1068  ifptru  1091  3mix1  1349  cad11  1646  19.33  1914  19.33b  1915  dfsb2  2525  moor  2582  ssun1  4132  reuun1  4282  opthpr  4817  prel12g  4830  opthprneg  4831  disjord  5099  el  5421  elelsuc  6438  ordssun  6467  fununmo  6585  tpres  7201  fvf1pr  7307  soxp  8126  poxp2  8140  poxp3  8147  omopth2  8570  naddunif  8681  swoord1  8728  swoord2  8729  nelaneqOLDOLD  9567  sornom  10262  fin56  10378  fpwwe2lem11  10627  ltle  11299  nn1m1nn  12255  elnnz  12602  elnn0z  12605  zmulcl  12644  nn01to3  12966  ltpnf  13146  xrltle  13175  xrltne  13189  swrdnnn0nd  14696  s3sndisj  15006  s3iunsndisj  15007  nn0o1gt2  16440  prm23lt5  16875  4sqlem17  17022  cshwsidrepswmod0  17155  cshwsdisj  17159  cshwshash  17165  funcres2c  17961  tsrlemax  18643  odlem1  19606  gexlem1  19650  drngmuleq0  20848  maducoeval2  22778  alexsubALTlem3  24187  dyadmbl  25740  gausslemma2dlem0f  27506  eln0s  28535  elnnzs  28575  bdayfinbndlem2  28642  nb3grprlem1  29711  frgrwopreg  30655  frgrregorufr  30657  2wspmdisj  30669  frgrregord13  30728  satfvsucsuc  35838  dfon2lem4  36257  dfrdg4  36424  btwnconn1  36574  segcon2  36578  broutsideof2  36595  lineunray  36620  meran1  36903  dissym1  36913  weiunpo  36957  axtco1from2  36967  bj-orim2  37129  bj-peircecurry  37131  bj-consensus  37152  bj-sbsb  37453  bj-unrab  37543  bj-axseprep  37692  wl-orel12  38147  orfa  38714  tsor2  38778  lkrlspeqN  39926  sbor2  42962  omcl3g  44044  fzunt  44164  fzuntd  44165  fzunt1d  44166  fzuntgd  44167  ifpid1g  44203  ifpim3  44205  rp-fakeanorass  44222  or3or  44732  clsk1indlem3  44752  ntrclsk3  44779  19.33-2  45075  ax6e2ndeq  45251  uunT1  45471  undif3VD  45573  ax6e2ndeqVD  45600  ax6e2ndeqALT  45622  salexct  47031  salexct3  47039  salgencntex  47040  salgensscntex  47041  ndmafv2nrn  47942  otiunsndisjX  47999  prproropf1olem4  48238  poprelb  48256  nn0o1gt2ALTV  48442  odd2prm2  48466  clnbgrel  48576  dfclnbgr6  48604  gpg5nbgrvtx03starlem2  48817  gpg5nbgrvtx13starlem2  48820  gpg5edgnedg  48878  ldepspr  49236  elfzolborelfzop1  49282  blen1b  49351  reorelicc  49473  opth1neg  49587  eximp-surprise2  50546