Theorem orc 385

Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.)

Assertion

Ref	Expression
orc	|- ( ph -> ( ph \/ ps ) )

Proof of Theorem orc

Step	Hyp	Ref	Expression
1		pm2.24 109	. 2 |- ( ph -> ( -. ph -> ps ) )
2	1	orrd 378	1 |- ( ph -> ( ph \/ ps ) )

Syntax hints:   -> wi 4   \/ wo 368

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 185  df-or 370

This theorem is referenced by:  pm1.4  386  orcd  392  orcs  394  pm2.45  397  pm2.67-2  402  biorfi  407  pm1.5  522  pm2.4  575  pm4.44  577  pm4.45  688  pm3.48  831  orabs  853  norbi  857  andi  865  pm4.72  874  biort  894  pm5.71  934  dedlema  952  consensus  957  3mix1  1165  cad1  1450  cad11  1451  cad0  1452  19.33  1672  19.33b  1673  dfsb2  2087  moor  2349  ssun1  3667  undif3  3759  reuun1  3780  opthpr  4204  otsndisj  4752  otiunsndisj  4753  elelsuc  4950  ordelinel  4976  ordssun  4977  ordequn  4978  fununmo  5631  soxp  6896  omopth2  7233  swoord1  7340  swoord2  7341  sornom  8657  fin56  8773  fpwwe2lem12  9019  ltle  9673  nn1m1nn  10556  elnnz  10874  elnn0z  10877  zmulcl  10911  nn01to3  11175  ltpnf  11331  xrltle  11355  xrltne  11366  4sqlem17  14338  cshwsidrepswmod0  14437  cshwsdisj  14441  cshwshash  14447  funcres2c  15128  tsrlemax  15707  odlem1  16365  gexlem1  16405  drngmuleq0  17219  maducoeval2  18937  alexsubALTlem3  20312  dyadmbl  21772  bcmono  23308  nb3graprlem1  24155  frgrawopreg  24754  frgraregorufr  24758  2spotdisj  24766  2spotiundisj  24767  2spotmdisj  24773  frgraregord13  24824  dfon2lem4  28823  sltsgn1  29026  sltsgn2  29027  dfrdg4  29205  btwnconn1  29356  segcon2  29360  broutsideof2  29377  lineunray  29402  meran1  29481  dissym1  29491  wl-nftht  29594  orfa  30110  tsim2  30170  tsim3  30171  tsbi3  30174  tsan2  30181  tsan3  30182  tsor2  30187  tsor3  30188  fnwe2lem3  30630  19.33-2  30893  fourierswlem  31559  otiunsndisjX  31796  ldepspr  32173  eximp-surprise2  32299  ax6e2ndeq  32430  uunT1  32675  undif3VD  32780  ax6e2ndeqVD  32807  ax6e2ndeqALT  32829  bj-dfif5ALT  33248  bj-consensus  33261  bj-unrab  33593  lkrlspeqN  33986