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  2528  moor  2585  ssun1  4134  reuun1  4284  opthpr  4821  prel12g  4834  opthprneg  4835  disjord  5103  el  5424  elelsuc  6443  ordssun  6472  fununmo  6590  tpres  7206  fvf1pr  7316  soxp  8134  poxp2  8148  poxp3  8155  omopth2  8578  naddunif  8689  swoord1  8736  swoord2  8737  nelaneqOLDOLD  9576  sornom  10279  fin56  10395  fpwwe2lem11  10644  ltle  11316  nn1m1nn  12272  elnnz  12619  elnn0z  12622  zmulcl  12661  nn01to3  12983  ltpnf  13163  xrltle  13192  xrltne  13206  swrdnnn0nd  14718  s3sndisj  15030  s3iunsndisj  15031  nn0o1gt2  16464  prm23lt5  16899  4sqlem17  17046  cshwsidrepswmod0  17179  cshwsdisj  17183  cshwshash  17189  funcres2c  17985  tsrlemax  18667  odlem1  19636  gexlem1  19680  drngmuleq0  20903  maducoeval2  22834  alexsubALTlem3  24243  dyadmbl  25796  gausslemma2dlem0f  27562  eln0s  28591  elnnzs  28631  bdayfinbndlem2  28698  nb3grprlem1  29767  frgrwopreg  30711  frgrregorufr  30713  2wspmdisj  30725  frgrregord13  30784  satfvsucsuc  35878  dfon2lem4  36297  dfrdg4  36464  btwnconn1  36614  segcon2  36618  broutsideof2  36635  lineunray  36660  meran1  36963  dissym1  36973  weiunpo  37017  axtco1from2  37027  bj-orim2  37189  bj-peircecurry  37191  bj-consensus  37212  bj-sbsb  37513  bj-unrab  37603  bj-axseprep  37752  wl-orel12  38207  orfa  38774  tsor2  38838  lkrlspeqN  39986  sbor2  43022  omcl3g  44102  fzunt  44222  fzuntd  44223  fzunt1d  44224  fzuntgd  44225  ifpid1g  44261  ifpim3  44263  rp-fakeanorass  44280  or3or  44790  clsk1indlem3  44810  ntrclsk3  44837  19.33-2  45133  ax6e2ndeq  45309  uunT1  45529  undif3VD  45631  ax6e2ndeqVD  45658  ax6e2ndeqALT  45680  salexct  47089  salexct3  47097  salgencntex  47098  salgensscntex  47099  ndmafv2nrn  48000  otiunsndisjX  48057  prproropf1olem4  48296  poprelb  48314  nn0o1gt2ALTV  48500  odd2prm2  48524  clnbgrel  48634  dfclnbgr6  48662  gpg5nbgrvtx03starlem2  48875  gpg5nbgrvtx13starlem2  48878  gpg5edgnedg  48936  ldepspr  49294  elfzolborelfzop1  49340  blen1b  49409  reorelicc  49531  opth1neg  49645  eximp-surprise2  50604