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  1616  19.33  1884  19.33b  1885  dfsb2  2497  moor  2553  ssun1  4153  reuun1  4303  opthpr  4827  prel12g  4840  opthprneg  4841  disjord  5108  elelsuc  6426  ordssun  6455  fununmo  6582  tpres  7192  fvf1pr  7299  soxp  8126  poxp2  8140  poxp3  8147  omopth2  8594  naddunif  8703  swoord1  8749  swoord2  8750  nelaneq  9611  sornom  10289  fin56  10405  fpwwe2lem11  10653  ltle  11321  nn1m1nn  12259  elnnz  12596  elnn0z  12599  zmulcl  12639  nn01to3  12955  ltpnf  13134  xrltle  13163  xrltne  13177  swrdnnn0nd  14672  s3sndisj  14984  s3iunsndisj  14985  nn0o1gt2  16398  prm23lt5  16832  4sqlem17  16979  cshwsidrepswmod0  17112  cshwsdisj  17116  cshwshash  17122  funcres2c  17914  tsrlemax  18594  odlem1  19514  gexlem1  19558  drngmuleq0  20721  maducoeval2  22576  alexsubALTlem3  23985  dyadmbl  25551  gausslemma2dlem0f  27322  eln0s  28275  elnnzs  28304  nb3grprlem1  29305  frgrwopreg  30250  frgrregorufr  30252  2wspmdisj  30264  frgrregord13  30323  satfvsucsuc  35333  dfon2lem4  35750  dfrdg4  35915  btwnconn1  36065  segcon2  36069  broutsideof2  36086  lineunray  36111  meran1  36375  dissym1  36385  weiunpo  36429  bj-orim2  36520  bj-peircecurry  36522  bj-consensus  36542  bj-sbsb  36801  bj-unrab  36890  wl-orel12  37475  orfa  38052  tsor2  38118  lkrlspeqN  39135  sbor2  42209  omcl3g  43305  fzunt  43426  fzuntd  43427  fzunt1d  43428  fzuntgd  43429  ifpid1g  43465  ifpim3  43467  rp-fakeanorass  43484  or3or  43994  clsk1indlem3  44014  ntrclsk3  44041  19.33-2  44354  ax6e2ndeq  44532  uunT1  44752  undif3VD  44854  ax6e2ndeqVD  44881  ax6e2ndeqALT  44903  salexct  46311  salexct3  46319  salgencntex  46320  salgensscntex  46321  ndmafv2nrn  47199  otiunsndisjX  47256  prproropf1olem4  47468  poprelb  47486  nn0o1gt2ALTV  47656  odd2prm2  47680  clnbgrel  47790  dfclnbgr6  47817  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx13starlem2  48022  ldepspr  48397  elfzolborelfzop1  48443  blen1b  48516  reorelicc  48638  opth1neg  48752  eximp-surprise2  49597