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  1616  19.33  1884  19.33b  1885  dfsb2  2491  moor  2547  ssun1  4131  reuun1  4281  opthpr  4805  prel12g  4818  opthprneg  4819  disjord  5084  elelsuc  6386  ordssun  6415  fununmo  6533  tpres  7141  fvf1pr  7248  soxp  8069  poxp2  8083  poxp3  8090  omopth2  8509  naddunif  8618  swoord1  8664  swoord2  8665  nelaneqOLD  9513  sornom  10190  fin56  10306  fpwwe2lem11  10554  ltle  11222  nn1m1nn  12167  elnnz  12499  elnn0z  12502  zmulcl  12542  nn01to3  12860  ltpnf  13040  xrltle  13069  xrltne  13083  swrdnnn0nd  14581  s3sndisj  14892  s3iunsndisj  14893  nn0o1gt2  16310  prm23lt5  16744  4sqlem17  16891  cshwsidrepswmod0  17024  cshwsdisj  17028  cshwshash  17034  funcres2c  17828  tsrlemax  18510  odlem1  19432  gexlem1  19476  drngmuleq0  20666  maducoeval2  22543  alexsubALTlem3  23952  dyadmbl  25517  gausslemma2dlem0f  27288  eln0s  28274  elnnzs  28312  nb3grprlem1  29343  frgrwopreg  30285  frgrregorufr  30287  2wspmdisj  30299  frgrregord13  30358  satfvsucsuc  35337  dfon2lem4  35759  dfrdg4  35924  btwnconn1  36074  segcon2  36078  broutsideof2  36095  lineunray  36120  meran1  36384  dissym1  36394  weiunpo  36438  bj-orim2  36529  bj-peircecurry  36531  bj-consensus  36551  bj-sbsb  36810  bj-unrab  36899  wl-orel12  37484  orfa  38061  tsor2  38127  lkrlspeqN  39149  sbor2  42185  omcl3g  43307  fzunt  43428  fzuntd  43429  fzunt1d  43430  fzuntgd  43431  ifpid1g  43467  ifpim3  43469  rp-fakeanorass  43486  or3or  43996  clsk1indlem3  44016  ntrclsk3  44043  19.33-2  44355  ax6e2ndeq  44533  uunT1  44753  undif3VD  44855  ax6e2ndeqVD  44882  ax6e2ndeqALT  44904  salexct  46316  salexct3  46324  salgencntex  46325  salgensscntex  46326  ndmafv2nrn  47207  otiunsndisjX  47264  prproropf1olem4  47491  poprelb  47509  nn0o1gt2ALTV  47679  odd2prm2  47703  clnbgrel  47813  dfclnbgr6  47841  gpg5nbgrvtx03starlem2  48054  gpg5nbgrvtx13starlem2  48057  gpg5edgnedg  48115  ldepspr  48459  elfzolborelfzop1  48505  blen1b  48574  reorelicc  48696  opth1neg  48811  eximp-surprise2  49771