Theorem orc 881

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 877	1 ⊢ (𝜑 → (𝜑 ∨ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm1.4  883  orcd  887  orcs  889  pm2.45  895  norbi  900  pm2.67-2  905  pm2.4  920  pm1.5  933  biort  949  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  1649  19.33  1917  19.33b  1918  dfsb2  2524  moor  2581  ssun1  4127  reuun1  4277  opthpr  4814  prel12g  4827  opthprneg  4828  disjord  5096  el  5417  elelsuc  6437  ordssun  6466  fununmo  6584  tpres  7204  fvf1pr  7312  soxp  8131  poxp2  8145  poxp3  8152  omopth2  8575  naddunif  8686  swoord1  8733  swoord2  8734  nelaneqOLDOLD  9580  sornom  10283  fin56  10399  fpwwe2lem11  10654  ltle  11326  nn1m1nn  12282  elnnz  12629  elnn0z  12632  zmulcl  12671  nn01to3  12994  ltpnf  13175  xrltle  13204  xrltne  13218  swrdnnn0nd  14730  s3sndisj  15044  s3iunsndisj  15045  nn0o1gt2  16477  prm23lt5  16912  4sqlem17  17059  cshwsidrepswmod0  17192  cshwsdisj  17196  cshwshash  17202  funcres2c  17998  tsrlemax  18680  odlem1  19668  gexlem1  19712  drngmuleq0  20935  maducoeval2  22868  alexsubALTlem3  24281  dyadmbl  25834  gausslemma2dlem0f  27605  eln0s  28634  elnnzs  28674  bdayfinbndlem2  28741  nb3grprlem1  29848  frgrwopreg  30811  frgrregorufr  30813  2wspmdisj  30825  frgrregord13  30884  satfvsucsuc  35952  dfon2lem4  36371  dfrdg4  36538  btwnconn1  36689  segcon2  36693  broutsideof2  36710  lineunray  36735  meran1  37038  dissym1  37048  weiunpo  37092  axtco1from2  37102  bj-orim2  37264  bj-peircecurry  37266  bj-consensus  37287  bj-sbsb  37588  bj-unrab  37678  bj-axseprep  37827  wl-orel12  38282  orfa  38840  tsor2  38904  lkrlspeqN  40052  sbor2  43088  omcl3g  44183  fzunt  44303  fzuntd  44304  fzunt1d  44305  fzuntgd  44306  ifpid1g  44342  ifpim3  44344  rp-fakeanorass  44361  or3or  44871  clsk1indlem3  44891  ntrclsk3  44918  19.33-2  45214  ax6e2ndeq  45390  uunT1  45610  undif3VD  45712  ax6e2ndeqVD  45739  ax6e2ndeqALT  45761  salexct  47170  salexct3  47178  salgencntex  47179  salgensscntex  47180  ndmafv2nrn  48118  otiunsndisjX  48175  prproropf1olem4  48414  poprelb  48432  nn0o1gt2ALTV  48618  odd2prm2  48642  clnbgrel  48752  dfclnbgr6  48780  gpg5nbgrvtx03starlem2  48993  gpg5nbgrvtx13starlem2  48996  gpg5edgnedg  49054  ldepspr  49411  elfzolborelfzop1  49457  blen1b  49526  reorelicc  49648  opth1neg  49762  eximp-surprise2  50722