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  1331  norasslem2  1535  cad11  1616  19.33  1884  19.33b  1885  dfsb2  2498  moor  2554  ssun1  4178  reuun1  4328  opthpr  4851  prel12g  4864  opthprneg  4865  disjord  5132  elelsuc  6457  ordssun  6486  fununmo  6613  tpres  7221  fvf1pr  7327  soxp  8154  poxp2  8168  poxp3  8175  omopth2  8622  naddunif  8731  swoord1  8777  swoord2  8778  nelaneq  9639  sornom  10317  fin56  10433  fpwwe2lem11  10681  ltle  11349  nn1m1nn  12287  elnnz  12623  elnn0z  12626  zmulcl  12666  nn01to3  12983  ltpnf  13162  xrltle  13191  xrltne  13205  swrdnnn0nd  14694  s3sndisj  15006  s3iunsndisj  15007  nn0o1gt2  16418  prm23lt5  16852  4sqlem17  16999  cshwsidrepswmod0  17132  cshwsdisj  17136  cshwshash  17142  funcres2c  17948  tsrlemax  18631  odlem1  19553  gexlem1  19597  drngmuleq0  20763  maducoeval2  22646  alexsubALTlem3  24057  dyadmbl  25635  gausslemma2dlem0f  27405  eln0s  28358  elnnzs  28387  nb3grprlem1  29397  frgrwopreg  30342  frgrregorufr  30344  2wspmdisj  30356  frgrregord13  30415  satfvsucsuc  35370  dfon2lem4  35787  dfrdg4  35952  btwnconn1  36102  segcon2  36106  broutsideof2  36123  lineunray  36148  meran1  36412  dissym1  36422  weiunpo  36466  bj-orim2  36557  bj-peircecurry  36559  bj-consensus  36579  bj-sbsb  36838  bj-unrab  36927  wl-orel12  37512  orfa  38089  tsor2  38155  lkrlspeqN  39172  sbor2  42251  omcl3g  43347  fzunt  43468  fzuntd  43469  fzunt1d  43470  fzuntgd  43471  ifpid1g  43507  ifpim3  43509  rp-fakeanorass  43526  or3or  44036  clsk1indlem3  44056  ntrclsk3  44083  19.33-2  44401  ax6e2ndeq  44579  uunT1  44800  undif3VD  44902  ax6e2ndeqVD  44929  ax6e2ndeqALT  44951  salexct  46349  salexct3  46357  salgencntex  46358  salgensscntex  46359  ndmafv2nrn  47234  otiunsndisjX  47291  prproropf1olem4  47493  poprelb  47511  nn0o1gt2ALTV  47681  odd2prm2  47705  clnbgrel  47815  dfclnbgr6  47842  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx13starlem2  48028  ldepspr  48390  elfzolborelfzop1  48436  blen1b  48509  reorelicc  48631  opth1neg  48739  eximp-surprise2  49304