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  2491  moor  2547  ssun1  4141  reuun1  4291  opthpr  4815  prel12g  4828  opthprneg  4829  disjord  5096  elelsuc  6407  ordssun  6436  fununmo  6563  tpres  7175  fvf1pr  7282  soxp  8108  poxp2  8122  poxp3  8129  omopth2  8548  naddunif  8657  swoord1  8703  swoord2  8704  nelaneq  9552  sornom  10230  fin56  10346  fpwwe2lem11  10594  ltle  11262  nn1m1nn  12207  elnnz  12539  elnn0z  12542  zmulcl  12582  nn01to3  12900  ltpnf  13080  xrltle  13109  xrltne  13123  swrdnnn0nd  14621  s3sndisj  14933  s3iunsndisj  14934  nn0o1gt2  16351  prm23lt5  16785  4sqlem17  16932  cshwsidrepswmod0  17065  cshwsdisj  17069  cshwshash  17075  funcres2c  17865  tsrlemax  18545  odlem1  19465  gexlem1  19509  drngmuleq0  20672  maducoeval2  22527  alexsubALTlem3  23936  dyadmbl  25501  gausslemma2dlem0f  27272  eln0s  28251  elnnzs  28289  nb3grprlem1  29307  frgrwopreg  30252  frgrregorufr  30254  2wspmdisj  30266  frgrregord13  30325  satfvsucsuc  35352  dfon2lem4  35774  dfrdg4  35939  btwnconn1  36089  segcon2  36093  broutsideof2  36110  lineunray  36135  meran1  36399  dissym1  36409  weiunpo  36453  bj-orim2  36544  bj-peircecurry  36546  bj-consensus  36566  bj-sbsb  36825  bj-unrab  36914  wl-orel12  37499  orfa  38076  tsor2  38142  lkrlspeqN  39164  sbor2  42200  omcl3g  43323  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  ifpid1g  43483  ifpim3  43485  rp-fakeanorass  43502  or3or  44012  clsk1indlem3  44032  ntrclsk3  44059  19.33-2  44371  ax6e2ndeq  44549  uunT1  44769  undif3VD  44871  ax6e2ndeqVD  44898  ax6e2ndeqALT  44920  salexct  46332  salexct3  46340  salgencntex  46341  salgensscntex  46342  ndmafv2nrn  47223  otiunsndisjX  47280  prproropf1olem4  47507  poprelb  47525  nn0o1gt2ALTV  47695  odd2prm2  47719  clnbgrel  47829  dfclnbgr6  47856  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx13starlem2  48063  ldepspr  48462  elfzolborelfzop1  48508  blen1b  48577  reorelicc  48699  opth1neg  48814  eximp-surprise2  49774