Theorem orc 865

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

Syntax hints:   → wi 4   ∨ wo 845

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 846

This theorem is referenced by:  pm1.4  867  orcd  871  orcs  873  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  1072  3mix1  1327  norasslem2  1528  cad11  1609  cad0OLD  1612  19.33  1879  19.33b  1880  dfsb2  2487  moor  2543  ssun1  4172  reuun1  4319  opthpr  4855  prel12g  4867  opthprneg  4868  disjord  5138  elelsuc  6445  ordssun  6474  fununmo  6603  tpres  7217  soxp  8138  poxp2  8152  poxp3  8159  omopth2  8609  naddunif  8718  swoord1  8760  swoord2  8761  nelaneq  9628  sornom  10306  fin56  10422  fpwwe2lem11  10670  ltle  11338  nn1m1nn  12269  elnnz  12604  elnn0z  12607  zmulcl  12647  nn01to3  12961  ltpnf  13138  xrltle  13166  xrltne  13180  swrdnnn0nd  14644  s3sndisj  14952  s3iunsndisj  14953  nn0o1gt2  16363  prm23lt5  16788  4sqlem17  16935  cshwsidrepswmod0  17069  cshwsdisj  17073  cshwshash  17079  funcres2c  17895  tsrlemax  18583  odlem1  19495  gexlem1  19539  drngmuleq0  20660  maducoeval2  22560  alexsubALTlem3  23971  dyadmbl  25547  gausslemma2dlem0f  27312  nb3grprlem1  29211  frgrwopreg  30151  frgrregorufr  30153  2wspmdisj  30165  frgrregord13  30224  satfvsucsuc  34980  dfon2lem4  35387  dfrdg4  35552  btwnconn1  35702  segcon2  35706  broutsideof2  35723  lineunray  35748  meran1  35900  dissym1  35910  bj-orim2  36036  bj-peircecurry  36038  bj-consensus  36059  bj-sbsb  36319  bj-unrab  36409  wl-orel12  36983  orfa  37560  tsor2  37626  lkrlspeqN  38647  sbor2  41703  omcl3g  42766  fzunt  42888  fzuntd  42889  fzunt1d  42890  fzuntgd  42891  ifpid1g  42927  ifpim3  42929  rp-fakeanorass  42946  or3or  43456  clsk1indlem3  43476  ntrclsk3  43503  19.33-2  43822  ax6e2ndeq  44001  uunT1  44222  undif3VD  44324  ax6e2ndeqVD  44351  ax6e2ndeqALT  44373  salexct  45724  salexct3  45732  salgencntex  45733  salgensscntex  45734  ndmafv2nrn  46604  otiunsndisjX  46661  prproropf1olem4  46848  poprelb  46866  nn0o1gt2ALTV  47036  odd2prm2  47060  clnbgrel  47169  dfclnbgr6  47193  ldepspr  47592  elfzolborelfzop1  47638  blen1b  47712  reorelicc  47834  eximp-surprise2  48269