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 210  df-or 848

This theorem is referenced by:  pm1.4  869  orcd  873  orcs  875  pm2.45  882  norbi  887  pm2.67-2  892  pm2.4  907  pm1.5  920  biort  936  biorfi  939  pm4.72  950  pm3.48  964  pm4.44  997  pm4.45  998  orabs  999  pm5.61  1001  andi  1008  pm5.71  1028  dedlema  1046  consensus  1053  ifptru  1076  3mix1  1332  norasslem2  1537  cad11  1623  cad0OLD  1626  19.33  1892  19.33b  1893  dfsb2  2496  moor  2553  ssun1  4072  reuun1  4218  opthpr  4748  prel12g  4760  opthprneg  4761  disjord  5027  elelsuc  6263  ordssun  6290  fununmo  6405  tpres  6994  soxp  7874  omopth2  8290  swoord1  8400  swoord2  8401  nelaneq  9193  sornom  9856  fin56  9972  fpwwe2lem11  10220  ltle  10886  nn1m1nn  11816  elnnz  12151  elnn0z  12154  zmulcl  12191  nn01to3  12502  ltpnf  12677  xrltle  12704  xrltne  12718  swrdnnn0nd  14186  s3sndisj  14495  s3iunsndisj  14496  nn0o1gt2  15905  prm23lt5  16330  4sqlem17  16477  cshwsidrepswmod0  16611  cshwsdisj  16615  cshwshash  16621  funcres2c  17362  tsrlemax  18046  odlem1  18881  gexlem1  18922  drngmuleq0  19744  maducoeval2  21491  alexsubALTlem3  22900  dyadmbl  24451  gausslemma2dlem0f  26196  nb3grprlem1  27422  frgrwopreg  28360  frgrregorufr  28362  2wspmdisj  28374  frgrregord13  28433  satfvsucsuc  32994  dfon2lem4  33432  poxp2  33470  poxp3  33476  dfrdg4  33939  btwnconn1  34089  segcon2  34093  broutsideof2  34110  lineunray  34135  meran1  34286  dissym1  34296  bj-orim2  34422  bj-peircecurry  34424  bj-consensus  34445  bj-sbsb  34706  bj-unrab  34800  wl-orel12  35356  orfa  35926  tsor2  35992  lkrlspeqN  36871  sbor2  39840  ifpid1g  40727  ifpim3  40729  rp-fakeanorass  40746  or3or  41249  clsk1indlem3  41271  ntrclsk3  41298  19.33-2  41614  ax6e2ndeq  41793  uunT1  42014  undif3VD  42116  ax6e2ndeqVD  42143  ax6e2ndeqALT  42165  salexct  43491  salexct3  43499  salgencntex  43500  salgensscntex  43501  ndmafv2nrn  44329  otiunsndisjX  44386  prproropf1olem4  44574  poprelb  44592  nn0o1gt2ALTV  44762  odd2prm2  44786  ldepspr  45430  elfzolborelfzop1  45476  blen1b  45550  reorelicc  45672  eximp-surprise2  46103