Theorem orc 873

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

Syntax hints:   → wi 4   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  pm1.4  875  orcd  879  orcs  881  pm2.45  887  norbi  892  pm2.67-2  897  pm2.4  912  pm1.5  925  biort  941  biorfriOLD  946  pm4.72  957  pm3.48  971  pm4.44  1004  pm4.45  1005  orabs  1006  pm5.61  1008  andi  1015  pm5.71  1035  dedlema  1051  consensus  1058  ifptru  1080  3mix1  1337  cad11  1623  19.33  1891  19.33b  1892  dfsb2  2501  moor  2558  ssun1  4114  reuun1  4263  opthpr  4789  prel12g  4802  opthprneg  4803  disjord  5068  el  5384  elelsuc  6392  ordssun  6421  fununmo  6539  tpres  7152  fvf1pr  7258  soxp  8076  poxp2  8090  poxp3  8097  omopth2  8516  naddunif  8626  swoord1  8673  swoord2  8674  nelaneqOLDOLD  9516  sornom  10197  fin56  10313  fpwwe2lem11  10562  ltle  11232  nn1m1nn  12193  elnnz  12532  elnn0z  12535  zmulcl  12574  nn01to3  12889  ltpnf  13069  xrltle  13098  xrltne  13112  swrdnnn0nd  14617  s3sndisj  14927  s3iunsndisj  14928  nn0o1gt2  16348  prm23lt5  16783  4sqlem17  16930  cshwsidrepswmod0  17063  cshwsdisj  17067  cshwshash  17073  funcres2c  17868  tsrlemax  18550  odlem1  19508  gexlem1  19552  drngmuleq0  20742  maducoeval2  22630  alexsubALTlem3  24039  dyadmbl  25592  gausslemma2dlem0f  27349  eln0s  28378  elnnzs  28418  bdayfinbndlem2  28485  nb3grprlem1  29474  frgrwopreg  30418  frgrregorufr  30420  2wspmdisj  30432  frgrregord13  30491  satfvsucsuc  35600  dfon2lem4  36019  dfrdg4  36186  btwnconn1  36336  segcon2  36340  broutsideof2  36357  lineunray  36382  meran1  36646  dissym1  36656  weiunpo  36700  axtco1from2  36710  bj-orim2  36873  bj-peircecurry  36875  bj-consensus  36896  bj-sbsb  37197  bj-unrab  37286  bj-axseprep  37434  wl-orel12  37889  orfa  38456  tsor2  38522  lkrlspeqN  39670  sbor2  42704  omcl3g  43786  fzunt  43906  fzuntd  43907  fzunt1d  43908  fzuntgd  43909  ifpid1g  43945  ifpim3  43947  rp-fakeanorass  43964  or3or  44474  clsk1indlem3  44494  ntrclsk3  44521  19.33-2  44833  ax6e2ndeq  45010  uunT1  45230  undif3VD  45332  ax6e2ndeqVD  45359  ax6e2ndeqALT  45381  salexct  46784  salexct3  46792  salgencntex  46793  salgensscntex  46794  ndmafv2nrn  47692  otiunsndisjX  47749  prproropf1olem4  47988  poprelb  48006  nn0o1gt2ALTV  48192  odd2prm2  48216  clnbgrel  48326  dfclnbgr6  48354  gpg5nbgrvtx03starlem2  48567  gpg5nbgrvtx13starlem2  48570  gpg5edgnedg  48628  ldepspr  48971  elfzolborelfzop1  49017  blen1b  49086  reorelicc  49208  opth1neg  49323  eximp-surprise2  50282