Theorem orc 868

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

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  pm1.4  870  orcd  874  orcs  876  pm2.45  882  norbi  887  pm2.67-2  892  pm2.4  907  pm1.5  920  biort  936  biorfriOLD  941  pm4.72  952  pm3.48  966  pm4.44  999  pm4.45  1000  orabs  1001  pm5.61  1003  andi  1010  pm5.71  1030  dedlema  1046  consensus  1053  ifptru  1075  3mix1  1332  cad11  1618  19.33  1886  19.33b  1887  dfsb2  2498  moor  2555  ssun1  4132  reuun1  4282  opthpr  4809  prel12g  4822  opthprneg  4823  disjord  5089  elelsuc  6400  ordssun  6429  fununmo  6547  tpres  7157  fvf1pr  7263  soxp  8081  poxp2  8095  poxp3  8102  omopth2  8521  naddunif  8631  swoord1  8678  swoord2  8679  nelaneqOLD  9519  sornom  10199  fin56  10315  fpwwe2lem11  10564  ltle  11233  nn1m1nn  12178  elnnz  12510  elnn0z  12513  zmulcl  12552  nn01to3  12866  ltpnf  13046  xrltle  13075  xrltne  13089  swrdnnn0nd  14592  s3sndisj  14902  s3iunsndisj  14903  nn0o1gt2  16320  prm23lt5  16754  4sqlem17  16901  cshwsidrepswmod0  17034  cshwsdisj  17038  cshwshash  17044  funcres2c  17839  tsrlemax  18521  odlem1  19476  gexlem1  19520  drngmuleq0  20708  maducoeval2  22596  alexsubALTlem3  24005  dyadmbl  25569  gausslemma2dlem0f  27340  eln0s  28369  elnnzs  28409  bdayfinbndlem2  28476  nb3grprlem1  29465  frgrwopreg  30410  frgrregorufr  30412  2wspmdisj  30424  frgrregord13  30483  satfvsucsuc  35578  dfon2lem4  35997  dfrdg4  36164  btwnconn1  36314  segcon2  36318  broutsideof2  36335  lineunray  36360  meran1  36624  dissym1  36634  weiunpo  36678  bj-orim2  36777  bj-peircecurry  36779  bj-consensus  36799  bj-sbsb  37079  bj-unrab  37168  bj-axseprep  37316  wl-orel12  37760  orfa  38327  tsor2  38393  lkrlspeqN  39541  sbor2  42576  omcl3g  43685  fzunt  43805  fzuntd  43806  fzunt1d  43807  fzuntgd  43808  ifpid1g  43844  ifpim3  43846  rp-fakeanorass  43863  or3or  44373  clsk1indlem3  44393  ntrclsk3  44420  19.33-2  44732  ax6e2ndeq  44909  uunT1  45129  undif3VD  45231  ax6e2ndeqVD  45258  ax6e2ndeqALT  45280  salexct  46686  salexct3  46694  salgencntex  46695  salgensscntex  46696  ndmafv2nrn  47576  otiunsndisjX  47633  prproropf1olem4  47860  poprelb  47878  nn0o1gt2ALTV  48048  odd2prm2  48072  clnbgrel  48182  dfclnbgr6  48210  gpg5nbgrvtx03starlem2  48423  gpg5nbgrvtx13starlem2  48426  gpg5edgnedg  48484  ldepspr  48827  elfzolborelfzop1  48873  blen1b  48942  reorelicc  49064  opth1neg  49179  eximp-surprise2  50138