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  1919  19.33b  1920  dfsb2  2525  moor  2582  ssun1  4179  reuun1  4276  opthpr  4809  prel12g  4822  opthprneg  4823  disjord  5095  el  5411  elelsuc  6459  ordssun  6488  fununmo  6610  tpres  7233  fvf1pr  7341  soxp  8171  poxp2  8190  poxp3  8197  omopth2  8623  naddunif  8734  swoord1  8781  swoord2  8782  nelaneqOLDOLD  9628  sornom  10385  fin56  10501  fpwwe2lem11  10756  ltle  11428  nn1m1nn  12386  elnnz  12733  elnn0z  12736  zmulcl  12775  nn01to3  13098  ltpnf  13279  xrltle  13308  xrltne  13322  swrdnnn0nd  14837  s3sndisj  15152  s3iunsndisj  15153  nn0o1gt2  16583  prm23lt5  17024  4sqlem17  17171  cshwsidrepswmod0  17304  cshwsdisj  17308  cshwshash  17314  funcres2c  18110  tsrlemax  18792  odlem1  19782  gexlem1  19826  drngmuleq0  21053  maducoeval2  22988  alexsubALTlem3  24401  dyadmbl  25954  gausslemma2dlem0f  27721  eln0s  28780  elnnzs  28820  bdayfinbndlem2  28887  nb3grprlem1  29994  frgrwopreg  30957  frgrregorufr  30959  2wspmdisj  30971  frgrregord13  31030  j00smo  36018  maxssj0  36019  onf1onf1or  36064  satfvsucsuc  36310  dfon2lem4  36739  dfrdg4  36906  btwnconn1  37057  segcon2  37061  broutsideof2  37078  lineunray  37103  meran1  37390  dissym1  37400  weiunpo  37444  axtco1from2  37454  bj-orim2  37616  bj-peircecurry  37618  bj-consensus  37639  bj-sbsb  37940  bj-unrab  38030  bj-axseprep  38194  wl-orel12  38648  negprop  38848  impprop  38849  orfa  39219  tsor2  39283  lkrlspeqN  40431  sbor2  43468  omcl3g  44539  fzunt  44659  fzuntd  44660  fzunt1d  44661  fzuntgd  44662  ifpid1g  44698  ifpim3  44700  rp-fakeanorass  44717  or3or  45226  clsk1indlem3  45246  ntrclsk3  45273  19.33-2  45569  ax6e2ndeq  45744  uunT1  45964  undif3VD  46066  ax6e2ndeqVD  46093  ax6e2ndeqALT  46115  salexct  47559  salexct3  47567  salgencntex  47568  salgensscntex  47569  ndmafv2nrn  48507  otiunsndisjX  48564  prproropf1olem4  48803  poprelb  48821  nn0o1gt2ALTV  49007  odd2prm2  49031  clnbgrel  49141  dfclnbgr6  49169  gpg5nbgrvtx03starlem2  49382  gpg5nbgrvtx13starlem2  49385  gpg5edgnedg  49443  ldepspr  49800  elfzolborelfzop1  49846  blen1b  49915  reorelicc  50037  opth1neg  50152  eximp-surprise2  51193