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  1617  19.33  1885  19.33b  1886  dfsb2  2493  moor  2549  ssun1  4128  reuun1  4278  opthpr  4803  prel12g  4816  opthprneg  4817  disjord  5080  elelsuc  6381  ordssun  6410  fununmo  6528  tpres  7135  fvf1pr  7241  soxp  8059  poxp2  8073  poxp3  8080  omopth2  8499  naddunif  8608  swoord1  8654  swoord2  8655  nelaneqOLD  9488  sornom  10165  fin56  10281  fpwwe2lem11  10529  ltle  11198  nn1m1nn  12143  elnnz  12475  elnn0z  12478  zmulcl  12518  nn01to3  12836  ltpnf  13016  xrltle  13045  xrltne  13059  swrdnnn0nd  14561  s3sndisj  14871  s3iunsndisj  14872  nn0o1gt2  16289  prm23lt5  16723  4sqlem17  16870  cshwsidrepswmod0  17003  cshwsdisj  17007  cshwshash  17013  funcres2c  17807  tsrlemax  18489  odlem1  19445  gexlem1  19489  drngmuleq0  20676  maducoeval2  22553  alexsubALTlem3  23962  dyadmbl  25526  gausslemma2dlem0f  27297  eln0s  28285  elnnzs  28323  nb3grprlem1  29356  frgrwopreg  30298  frgrregorufr  30300  2wspmdisj  30312  frgrregord13  30371  satfvsucsuc  35397  dfon2lem4  35819  dfrdg4  35984  btwnconn1  36134  segcon2  36138  broutsideof2  36155  lineunray  36180  meran1  36444  dissym1  36454  weiunpo  36498  bj-orim2  36589  bj-peircecurry  36591  bj-consensus  36611  bj-sbsb  36870  bj-unrab  36959  wl-orel12  37544  orfa  38121  tsor2  38187  lkrlspeqN  39209  sbor2  42244  omcl3g  43366  fzunt  43487  fzuntd  43488  fzunt1d  43489  fzuntgd  43490  ifpid1g  43526  ifpim3  43528  rp-fakeanorass  43545  or3or  44055  clsk1indlem3  44075  ntrclsk3  44102  19.33-2  44414  ax6e2ndeq  44591  uunT1  44811  undif3VD  44913  ax6e2ndeqVD  44940  ax6e2ndeqALT  44962  salexct  46371  salexct3  46379  salgencntex  46380  salgensscntex  46381  ndmafv2nrn  47252  otiunsndisjX  47309  prproropf1olem4  47536  poprelb  47554  nn0o1gt2ALTV  47724  odd2prm2  47748  clnbgrel  47858  dfclnbgr6  47886  gpg5nbgrvtx03starlem2  48099  gpg5nbgrvtx13starlem2  48102  gpg5edgnedg  48160  ldepspr  48504  elfzolborelfzop1  48550  blen1b  48619  reorelicc  48741  opth1neg  48856  eximp-surprise2  49816