Theorem orc 866

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

Syntax hints:   → wi 4   ∨ wo 846

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 206  df-or 847

This theorem is referenced by:  pm1.4  868  orcd  872  orcs  874  pm2.45  881  norbi  886  pm2.67-2  891  pm2.4  906  pm1.5  919  biort  935  biorfi  938  pm4.72  949  pm3.48  963  pm4.44  996  pm4.45  997  orabs  998  pm5.61  1000  andi  1007  pm5.71  1027  dedlema  1045  consensus  1052  ifptru  1075  3mix1  1331  norasslem2  1537  cad11  1618  cad0OLD  1621  19.33  1888  19.33b  1889  dfsb2  2493  moor  2549  ssun1  4173  reuun1  4318  opthpr  4853  prel12g  4865  opthprneg  4866  disjord  5137  elelsuc  6438  ordssun  6467  fununmo  6596  tpres  7202  soxp  8115  poxp2  8129  poxp3  8136  omopth2  8584  naddunif  8692  swoord1  8734  swoord2  8735  nelaneq  9594  sornom  10272  fin56  10388  fpwwe2lem11  10636  ltle  11302  nn1m1nn  12233  elnnz  12568  elnn0z  12571  zmulcl  12611  nn01to3  12925  ltpnf  13100  xrltle  13128  xrltne  13142  swrdnnn0nd  14606  s3sndisj  14914  s3iunsndisj  14915  nn0o1gt2  16324  prm23lt5  16747  4sqlem17  16894  cshwsidrepswmod0  17028  cshwsdisj  17032  cshwshash  17038  funcres2c  17852  tsrlemax  18539  odlem1  19403  gexlem1  19447  drngmuleq0  20388  maducoeval2  22142  alexsubALTlem3  23553  dyadmbl  25117  gausslemma2dlem0f  26864  nb3grprlem1  28637  frgrwopreg  29576  frgrregorufr  29578  2wspmdisj  29590  frgrregord13  29649  satfvsucsuc  34356  dfon2lem4  34758  dfrdg4  34923  btwnconn1  35073  segcon2  35077  broutsideof2  35094  lineunray  35119  meran1  35296  dissym1  35306  bj-orim2  35432  bj-peircecurry  35434  bj-consensus  35455  bj-sbsb  35715  bj-unrab  35806  wl-orel12  36380  orfa  36950  tsor2  37016  lkrlspeqN  38041  sbor2  41028  omcl3g  42084  fzunt  42206  fzuntd  42207  fzunt1d  42208  fzuntgd  42209  ifpid1g  42245  ifpim3  42247  rp-fakeanorass  42264  or3or  42774  clsk1indlem3  42794  ntrclsk3  42821  19.33-2  43141  ax6e2ndeq  43320  uunT1  43541  undif3VD  43643  ax6e2ndeqVD  43670  ax6e2ndeqALT  43692  salexct  45050  salexct3  45058  salgencntex  45059  salgensscntex  45060  ndmafv2nrn  45930  otiunsndisjX  45987  prproropf1olem4  46174  poprelb  46192  nn0o1gt2ALTV  46362  odd2prm2  46386  ldepspr  47154  elfzolborelfzop1  47200  blen1b  47274  reorelicc  47396  eximp-surprise2  47832