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  37716  orfa  38283  tsor2  38349  lkrlspeqN  39441  sbor2  42476  omcl3g  43586  fzunt  43706  fzuntd  43707  fzunt1d  43708  fzuntgd  43709  ifpid1g  43745  ifpim3  43747  rp-fakeanorass  43764  or3or  44274  clsk1indlem3  44294  ntrclsk3  44321  19.33-2  44633  ax6e2ndeq  44810  uunT1  45030  undif3VD  45132  ax6e2ndeqVD  45159  ax6e2ndeqALT  45181  salexct  46588  salexct3  46596  salgencntex  46597  salgensscntex  46598  ndmafv2nrn  47478  otiunsndisjX  47535  prproropf1olem4  47762  poprelb  47780  nn0o1gt2ALTV  47950  odd2prm2  47974  clnbgrel  48084  dfclnbgr6  48112  gpg5nbgrvtx03starlem2  48325  gpg5nbgrvtx13starlem2  48328  gpg5edgnedg  48386  ldepspr  48729  elfzolborelfzop1  48775  blen1b  48844  reorelicc  48966  opth1neg  49081  eximp-surprise2  50040