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  829  orabs  851  norbi  855  andi  862  pm4.72  871  biort  891  pm5.71  927  dedlema  945  consensus  950  3mix1  1157  cad1  1440  cad11  1441  cad0  1442  19.33  1662  19.33b  1663  dfsb2  2064  moor  2327  ssun1  3517  undif3  3609  reuun1  3630  opthpr  4048  elelsuc  4789  ordelinel  4815  ordssun  4816  ordequn  4817  fununmo  5459  soxp  6683  omopth2  7021  swoord1  7128  swoord2  7129  sornom  8444  fin56  8560  fpwwe2lem12  8806  ltle  9461  nn1m1nn  10340  elnnz  10654  elnn0z  10657  zmulcl  10691  ltpnf  11100  xrltle  11124  xrltne  11135  4sqlem17  14020  cshwsidrepswmod0  14119  cshwsdisj  14123  cshwshash  14129  funcres2c  14809  tsrlemax  15388  odlem1  16036  gexlem1  16076  drngmuleq0  16853  maducoeval2  18444  alexsubALTlem3  19619  dyadmbl  21078  bcmono  22614  nb3graprlem1  23357  dfon2lem4  27597  sltsgn1  27800  sltsgn2  27801  dfrdg4  27979  btwnconn1  28130  segcon2  28134  broutsideof2  28151  lineunray  28176  meran1  28255  dissym1  28265  wl-nftht  28362  orfa  28879  tsim2  28939  tsim3  28940  tsbi3  28943  tsan2  28950  tsan3  28951  tsor2  28956  tsor3  28957  fnwe2lem3  29402  19.33-2  29631  otsndisj  30128  otiunsndisj  30129  otiunsndisjX  30130  nn01to3  30184  frgrawopreg  30639  frgraregorufr  30643  2spotdisj  30651  2spotiundisj  30652  2spotmdisj  30658  frgraregord13  30709  ldepspr  31004  eximp-surprise2  31134  ax6e2ndeq  31265  uunT1  31510  undif3VD  31615  ax6e2ndeqVD  31642  ax6e2ndeqALT  31664  bj-dfif5ALT  32083  bj-consensus  32096  bj-unrab  32426  lkrlspeqN  32813