Theorem orc 867

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

Syntax hints:   → wi 4   ∨ wo 847

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 848

This theorem is referenced by:  pm1.4  869  orcd  873  orcs  875  pm2.45  881  norbi  886  pm2.67-2  891  pm2.4  906  pm1.5  919  biort  935  biorfriOLD  940  pm4.72  951  pm3.48  965  pm4.44  998  pm4.45  999  orabs  1000  pm5.61  1002  andi  1009  pm5.71  1029  dedlema  1045  consensus  1052  ifptru  1074  3mix1  1331  cad11  1617  19.33  1885  19.33b  1886  dfsb2  2497  moor  2554  ssun1  4130  reuun1  4280  opthpr  4807  prel12g  4820  opthprneg  4821  disjord  5087  elelsuc  6392  ordssun  6421  fununmo  6539  tpres  7147  fvf1pr  7253  soxp  8071  poxp2  8085  poxp3  8092  omopth2  8511  naddunif  8621  swoord1  8667  swoord2  8668  nelaneqOLD  9507  sornom  10187  fin56  10303  fpwwe2lem11  10552  ltle  11221  nn1m1nn  12166  elnnz  12498  elnn0z  12501  zmulcl  12540  nn01to3  12854  ltpnf  13034  xrltle  13063  xrltne  13077  swrdnnn0nd  14580  s3sndisj  14890  s3iunsndisj  14891  nn0o1gt2  16308  prm23lt5  16742  4sqlem17  16889  cshwsidrepswmod0  17022  cshwsdisj  17026  cshwshash  17032  funcres2c  17827  tsrlemax  18509  odlem1  19464  gexlem1  19508  drngmuleq0  20696  maducoeval2  22584  alexsubALTlem3  23993  dyadmbl  25557  gausslemma2dlem0f  27328  eln0s  28357  elnnzs  28397  bdayfinbndlem2  28464  nb3grprlem1  29453  frgrwopreg  30398  frgrregorufr  30400  2wspmdisj  30412  frgrregord13  30471  satfvsucsuc  35559  dfon2lem4  35978  dfrdg4  36145  btwnconn1  36295  segcon2  36299  broutsideof2  36316  lineunray  36341  meran1  36605  dissym1  36615  weiunpo  36659  bj-orim2  36756  bj-peircecurry  36758  bj-consensus  36778  bj-sbsb  37038  bj-unrab  37127  wl-orel12  37712  orfa  38279  tsor2  38345  lkrlspeqN  39427  sbor2  42462  omcl3g  43572  fzunt  43692  fzuntd  43693  fzunt1d  43694  fzuntgd  43695  ifpid1g  43731  ifpim3  43733  rp-fakeanorass  43750  or3or  44260  clsk1indlem3  44280  ntrclsk3  44307  19.33-2  44619  ax6e2ndeq  44796  uunT1  45016  undif3VD  45118  ax6e2ndeqVD  45145  ax6e2ndeqALT  45167  salexct  46574  salexct3  46582  salgencntex  46583  salgensscntex  46584  ndmafv2nrn  47464  otiunsndisjX  47521  prproropf1olem4  47748  poprelb  47766  nn0o1gt2ALTV  47936  odd2prm2  47960  clnbgrel  48070  dfclnbgr6  48098  gpg5nbgrvtx03starlem2  48311  gpg5nbgrvtx13starlem2  48314  gpg5edgnedg  48372  ldepspr  48715  elfzolborelfzop1  48761  blen1b  48830  reorelicc  48952  opth1neg  49067  eximp-surprise2  50026