Theorem orc 386

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 112	. 2 |- ( ph -> ( -. ph -> ps ) )
2	1	orrd 379	1 |- ( ph -> ( ph \/ ps ) )

Syntax hints:   -> wi 4   \/ wo 369

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 188  df-or 371

This theorem is referenced by:  pm1.4  387  orcd  393  orcs  395  pm2.45  398  pm2.67-2  403  biorfi  408  pm1.5  524  pm2.4  577  pm4.44  579  pm4.45  692  pm3.48  841  orabs  863  norbi  867  andi  875  pm4.72  884  biort  904  pm5.71  944  dedlema  962  consensus  967  3mix1  1174  ifptru  1431  cad0  1515  cad11  1517  19.33  1739  19.33b  1740  dfsb2  2165  moor  2320  ssun1  3626  undif3  3731  reuun1  3752  eqoreldif  4035  opthpr  4172  otsndisj  4717  otiunsndisj  4718  elelsuc  5505  ordelinel  5531  ordssun  5532  ordequn  5533  fununmo  5635  tpres  6123  soxp  6911  omopth2  7284  swoord1  7391  swoord2  7392  sornom  8696  fin56  8812  fpwwe2lem12  9055  ltle  9711  nn1m1nn  10618  elnnz  10936  elnn0z  10939  zmulcl  10974  nn01to3  11246  ltpnf  11411  xrltle  11437  xrltne  11449  4sqlem17OLD  14857  4sqlem17  14863  cshwsidrepswmod0  15017  cshwsdisj  15021  cshwshash  15027  funcres2c  15750  tsrlemax  16410  odlem1  17119  gexlem1  17159  drngmuleq0  17926  maducoeval2  19589  alexsubALTlem3  20988  dyadmbl  22432  bcmono  24065  nb3graprlem1  25021  frgrawopreg  25619  frgraregorufr  25623  2spotdisj  25631  2spotiundisj  25632  2spotmdisj  25638  frgraregord13  25689  dfon2lem4  30216  sltsgn1  30332  sltsgn2  30333  dfrdg4  30500  btwnconn1  30650  segcon2  30654  broutsideof2  30671  lineunray  30696  meran1  30853  dissym1  30863  bj-consensus  30938  bj-unrab  31276  wl-orel12  31553  wl-nftht  31573  orfa  32019  tsor2  32094  lkrlspeqN  32446  fnwe2lem3  35620  ifpid1g  35841  ifpim3  35843  rp-fakeanorass  35860  19.33-2  36372  ax6e2ndeq  36567  uunT1  36811  undif3VD  36923  ax6e2ndeqVD  36950  ax6e2ndeqALT  36972  nnfoctbdjlem  37806  nn0o1gt2ALTV  38226  otiunsndisjX  38391  ldepspr  39039  elfzolborelfzop1  39090  nn0o1gt2  39101  blen1b  39173  eximp-surprise2  39298