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  1533  cad11  1618  cad0OLD  1621  19.33  1887  19.33b  1888  dfsb2  2497  moor  2554  ssun1  4106  reuun1  4251  opthpr  4782  prel12g  4794  opthprneg  4795  disjord  5062  elelsuc  6338  ordssun  6365  fununmo  6481  tpres  7076  soxp  7970  omopth2  8415  swoord1  8529  swoord2  8530  nelaneq  9358  sornom  10033  fin56  10149  fpwwe2lem11  10397  ltle  11063  nn1m1nn  11994  elnnz  12329  elnn0z  12332  zmulcl  12369  nn01to3  12681  ltpnf  12856  xrltle  12883  xrltne  12897  swrdnnn0nd  14369  s3sndisj  14678  s3iunsndisj  14679  nn0o1gt2  16090  prm23lt5  16515  4sqlem17  16662  cshwsidrepswmod0  16796  cshwsdisj  16800  cshwshash  16806  funcres2c  17617  tsrlemax  18304  odlem1  19143  gexlem1  19184  drngmuleq0  20014  maducoeval2  21789  alexsubALTlem3  23200  dyadmbl  24764  gausslemma2dlem0f  26509  nb3grprlem1  27747  frgrwopreg  28687  frgrregorufr  28689  2wspmdisj  28701  frgrregord13  28760  satfvsucsuc  33327  dfon2lem4  33762  poxp2  33790  poxp3  33796  dfrdg4  34253  btwnconn1  34403  segcon2  34407  broutsideof2  34424  lineunray  34449  meran1  34600  dissym1  34610  bj-orim2  34736  bj-peircecurry  34738  bj-consensus  34759  bj-sbsb  35020  bj-unrab  35114  wl-orel12  35670  orfa  36240  tsor2  36306  lkrlspeqN  37185  sbor2  40177  fzunt  41062  fzuntd  41063  fzunt1d  41064  fzuntgd  41065  ifpid1g  41101  ifpim3  41103  rp-fakeanorass  41120  or3or  41631  clsk1indlem3  41653  ntrclsk3  41680  19.33-2  42000  ax6e2ndeq  42179  uunT1  42400  undif3VD  42502  ax6e2ndeqVD  42529  ax6e2ndeqALT  42551  salexct  43873  salexct3  43881  salgencntex  43882  salgensscntex  43883  ndmafv2nrn  44714  otiunsndisjX  44771  prproropf1olem4  44958  poprelb  44976  nn0o1gt2ALTV  45146  odd2prm2  45170  ldepspr  45814  elfzolborelfzop1  45860  blen1b  45934  reorelicc  46056  eximp-surprise2  46489