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  1648  19.33  1916  19.33b  1917  dfsb2  2522  moor  2579  ssun1  4176  reuun1  4273  opthpr  4805  prel12g  4818  opthprneg  4819  disjord  5091  el  5405  elelsuc  6438  ordssun  6467  fununmo  6587  tpres  7207  fvf1pr  7315  soxp  8143  poxp2  8162  poxp3  8169  omopth2  8595  naddunif  8706  swoord1  8753  swoord2  8754  nelaneqOLDOLD  9601  sornom  10358  fin56  10474  fpwwe2lem11  10729  ltle  11401  nn1m1nn  12359  elnnz  12706  elnn0z  12709  zmulcl  12748  nn01to3  13071  ltpnf  13252  xrltle  13281  xrltne  13295  swrdnnn0nd  14810  s3sndisj  15125  s3iunsndisj  15126  nn0o1gt2  16556  prm23lt5  16997  4sqlem17  17144  cshwsidrepswmod0  17277  cshwsdisj  17281  cshwshash  17287  funcres2c  18083  tsrlemax  18765  odlem1  19754  gexlem1  19798  drngmuleq0  21025  maducoeval2  22960  alexsubALTlem3  24373  dyadmbl  25926  gausslemma2dlem0f  27693  eln0s  28752  elnnzs  28792  bdayfinbndlem2  28859  nb3grprlem1  29966  frgrwopreg  30929  frgrregorufr  30931  2wspmdisj  30943  frgrregord13  31002  j00smo  35944  maxssj0  35945  onf1onf1or  35970  satfvsucsuc  36216  dfon2lem4  36640  dfrdg4  36807  btwnconn1  36958  segcon2  36962  broutsideof2  36979  lineunray  37004  meran1  37291  dissym1  37301  weiunpo  37345  axtco1from2  37355  bj-orim2  37517  bj-peircecurry  37519  bj-consensus  37540  bj-sbsb  37841  bj-unrab  37931  bj-axseprep  38082  wl-orel12  38536  negprop  38736  impprop  38737  orfa  39109  tsor2  39173  lkrlspeqN  40321  sbor2  43357  omcl3g  44429  fzunt  44549  fzuntd  44550  fzunt1d  44551  fzuntgd  44552  ifpid1g  44588  ifpim3  44590  rp-fakeanorass  44607  or3or  45116  clsk1indlem3  45136  ntrclsk3  45163  19.33-2  45459  ax6e2ndeq  45635  uunT1  45855  undif3VD  45957  ax6e2ndeqVD  45984  ax6e2ndeqALT  46006  salexct  47437  salexct3  47445  salgencntex  47446  salgensscntex  47447  ndmafv2nrn  48385  otiunsndisjX  48442  prproropf1olem4  48681  poprelb  48699  nn0o1gt2ALTV  48885  odd2prm2  48909  clnbgrel  49019  dfclnbgr6  49047  gpg5nbgrvtx03starlem2  49260  gpg5nbgrvtx13starlem2  49263  gpg5edgnedg  49321  ldepspr  49678  elfzolborelfzop1  49724  blen1b  49793  reorelicc  49915  opth1neg  50030  eximp-surprise2  51049