Theorem adantrl 478

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
adantrl	|- ( ( ph /\ ( th /\ ps ) ) -> ch )

Proof of Theorem adantrl

Step	Hyp	Ref	Expression
1		simpr 110	. 2 |- ( ( th /\ ps ) -> ps )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan2 286	1 |- ( ( ph /\ ( th /\ ps ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  ad2ant2l  508  ad2ant2rl  511  3ad2antr2  1189  3ad2antr3  1190  xordidc  1443  opabssxpd  4762  foco  5571  fvun1  5713  isocnv  5955  isores2  5957  f1oiso2  5971  offval  6246  xp2nd  6332  1stconst  6389  2ndconst  6390  tfrlem9  6488  nnmordi  6687  dom2lem  6948  fundmen  6984  mapen  7035  ssenen  7040  ltsonq  7621  ltexnqq  7631  genprndl  7744  genprndu  7745  ltpopr  7818  ltsopr  7819  ltexprlemm  7823  ltexprlemopl  7824  ltexprlemopu  7826  ltexprlemdisj  7829  ltexprlemfl  7832  ltexprlemfu  7834  mulcmpblnrlemg  7963  cnegexlem2  8358  muladd  8566  eqord1  8666  eqord2  8667  divadddivap  8910  ltmul12a  9043  lemul12b  9044  cju  9144  zextlt  9575  supinfneg  9832  infsupneg  9833  xrre  10058  ixxdisj  10141  iooshf  10190  icodisj  10230  iccshftr  10232  iccshftl  10234  iccdil  10236  icccntr  10238  iccf1o  10242  fzaddel  10297  fzsubel  10298  seq3caopr  10761  seqcaoprg  10762  expineg2  10814  expsubap  10853  expnbnd  10929  facndiv  11005  hashfacen  11104  ccatpfx  11289  swrdccatfn  11312  swrdccatin2  11317  fprodeq0  12199  lcmdvds  12672  hashdvds  12814  eulerthlemh  12824  pceu  12889  pcqcl  12900  infpnlem1  12953  4sqlem11  12995  mhmpropd  13570  subsubm  13587  grplcan  13666  grplmulf1o  13678  dfgrp3mlem  13702  mulgfng  13732  mulgsubcl  13744  subsubg  13805  eqger  13832  resghm  13868  conjghm  13884  subsubrng  14250  subsubrg  14281  psrbagconf1o  14714  psrgrp  14726  txlm  15030  blininf  15175  xmeter  15187  xmetresbl  15191  limcimo  15416  dvdsppwf1o  15740  fsumdvdsmul  15742  sgmmul  15747  clwwlkn1loopb  16298