Theorem orc 864

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

Syntax hints:   → wi 4   ∨ wo 844

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 845

This theorem is referenced by:  pm1.4  866  orcd  870  orcs  872  pm2.45  879  norbi  884  pm2.67-2  889  pm2.4  904  pm1.5  917  biort  933  biorfi  936  pm4.72  947  pm3.48  961  pm4.44  994  pm4.45  995  orabs  996  pm5.61  998  andi  1005  pm5.71  1025  dedlema  1043  consensus  1050  ifptru  1073  3mix1  1329  norasslem2  1536  cad11  1622  cad0OLD  1625  19.33  1891  19.33b  1892  dfsb2  2499  moor  2556  ssun1  4111  reuun1  4257  opthpr  4788  prel12g  4800  opthprneg  4801  disjord  5067  elelsuc  6337  ordssun  6364  fununmo  6479  tpres  7073  soxp  7961  omopth2  8400  swoord1  8512  swoord2  8513  nelaneq  9336  sornom  10034  fin56  10150  fpwwe2lem11  10398  ltle  11064  nn1m1nn  11994  elnnz  12329  elnn0z  12332  zmulcl  12369  nn01to3  12680  ltpnf  12855  xrltle  12882  xrltne  12896  swrdnnn0nd  14367  s3sndisj  14676  s3iunsndisj  14677  nn0o1gt2  16088  prm23lt5  16513  4sqlem17  16660  cshwsidrepswmod0  16794  cshwsdisj  16798  cshwshash  16804  funcres2c  17615  tsrlemax  18302  odlem1  19141  gexlem1  19182  drngmuleq0  20012  maducoeval2  21787  alexsubALTlem3  23198  dyadmbl  24762  gausslemma2dlem0f  26507  nb3grprlem1  27745  frgrwopreg  28683  frgrregorufr  28685  2wspmdisj  28697  frgrregord13  28756  satfvsucsuc  33323  dfon2lem4  33758  poxp2  33786  poxp3  33792  dfrdg4  34249  btwnconn1  34399  segcon2  34403  broutsideof2  34420  lineunray  34445  meran1  34596  dissym1  34606  bj-orim2  34732  bj-peircecurry  34734  bj-consensus  34755  bj-sbsb  35016  bj-unrab  35110  wl-orel12  35666  orfa  36236  tsor2  36302  lkrlspeqN  37181  sbor2  40174  ifpid1g  41080  ifpim3  41082  rp-fakeanorass  41099  or3or  41601  clsk1indlem3  41623  ntrclsk3  41650  19.33-2  41970  ax6e2ndeq  42149  uunT1  42370  undif3VD  42472  ax6e2ndeqVD  42499  ax6e2ndeqALT  42521  salexct  43844  salexct3  43852  salgencntex  43853  salgensscntex  43854  ndmafv2nrn  44682  otiunsndisjX  44739  prproropf1olem4  44927  poprelb  44945  nn0o1gt2ALTV  45115  odd2prm2  45139  ldepspr  45783  elfzolborelfzop1  45829  blen1b  45903  reorelicc  46025  eximp-surprise2  46458