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  2498  moor  2555  ssun1  4119  reuun1  4269  opthpr  4795  prel12g  4808  opthprneg  4809  disjord  5075  el  5385  elelsuc  6392  ordssun  6421  fununmo  6539  tpres  7149  fvf1pr  7255  soxp  8072  poxp2  8086  poxp3  8093  omopth2  8512  naddunif  8622  swoord1  8669  swoord2  8670  nelaneqOLD  9510  sornom  10190  fin56  10306  fpwwe2lem11  10555  ltle  11225  nn1m1nn  12186  elnnz  12525  elnn0z  12528  zmulcl  12567  nn01to3  12882  ltpnf  13062  xrltle  13091  xrltne  13105  swrdnnn0nd  14610  s3sndisj  14920  s3iunsndisj  14921  nn0o1gt2  16341  prm23lt5  16776  4sqlem17  16923  cshwsidrepswmod0  17056  cshwsdisj  17060  cshwshash  17066  funcres2c  17861  tsrlemax  18543  odlem1  19501  gexlem1  19545  drngmuleq0  20731  maducoeval2  22615  alexsubALTlem3  24024  dyadmbl  25577  gausslemma2dlem0f  27338  eln0s  28367  elnnzs  28407  bdayfinbndlem2  28474  nb3grprlem1  29463  frgrwopreg  30408  frgrregorufr  30410  2wspmdisj  30422  frgrregord13  30481  satfvsucsuc  35563  dfon2lem4  35982  dfrdg4  36149  btwnconn1  36299  segcon2  36303  broutsideof2  36320  lineunray  36345  meran1  36609  dissym1  36619  weiunpo  36663  axtco1from2  36673  bj-orim2  36836  bj-peircecurry  36838  bj-consensus  36859  bj-sbsb  37160  bj-unrab  37249  bj-axseprep  37397  wl-orel12  37850  orfa  38417  tsor2  38483  lkrlspeqN  39631  sbor2  42665  omcl3g  43780  fzunt  43900  fzuntd  43901  fzunt1d  43902  fzuntgd  43903  ifpid1g  43939  ifpim3  43941  rp-fakeanorass  43958  or3or  44468  clsk1indlem3  44488  ntrclsk3  44515  19.33-2  44827  ax6e2ndeq  45004  uunT1  45224  undif3VD  45326  ax6e2ndeqVD  45353  ax6e2ndeqALT  45375  salexct  46780  salexct3  46788  salgencntex  46789  salgensscntex  46790  ndmafv2nrn  47682  otiunsndisjX  47739  prproropf1olem4  47978  poprelb  47996  nn0o1gt2ALTV  48182  odd2prm2  48206  clnbgrel  48316  dfclnbgr6  48344  gpg5nbgrvtx03starlem2  48557  gpg5nbgrvtx13starlem2  48560  gpg5edgnedg  48618  ldepspr  48961  elfzolborelfzop1  49007  blen1b  49076  reorelicc  49198  opth1neg  49313  eximp-surprise2  50272