Theorem adantrl 475

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 109	. 2 |- ( ( th /\ ps ) -> ps )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan2 284	1 |- ( ( ph /\ ( th /\ ps ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  ad2ant2l  505  ad2ant2rl  508  3ad2antr2  1158  3ad2antr3  1159  xordidc  1394  foco  5430  fvun1  5562  isocnv  5790  isores2  5792  f1oiso2  5806  offval  6068  xp2nd  6145  1stconst  6200  2ndconst  6201  tfrlem9  6298  nnmordi  6495  dom2lem  6750  fundmen  6784  mapen  6824  ssenen  6829  ltsonq  7360  ltexnqq  7370  genprndl  7483  genprndu  7484  ltpopr  7557  ltsopr  7558  ltexprlemm  7562  ltexprlemopl  7563  ltexprlemopu  7565  ltexprlemdisj  7568  ltexprlemfl  7571  ltexprlemfu  7573  mulcmpblnrlemg  7702  cnegexlem2  8095  muladd  8303  eqord1  8402  eqord2  8403  divadddivap  8644  ltmul12a  8776  lemul12b  8777  cju  8877  zextlt  9304  supinfneg  9554  infsupneg  9555  xrre  9777  ixxdisj  9860  iooshf  9909  icodisj  9949  iccshftr  9951  iccshftl  9953  iccdil  9955  icccntr  9957  iccf1o  9961  fzaddel  10015  fzsubel  10016  seq3caopr  10439  expineg2  10485  expsubap  10524  expnbnd  10599  facndiv  10673  hashfacen  10771  fprodeq0  11580  lcmdvds  12033  hashdvds  12175  eulerthlemh  12185  pceu  12249  pcqcl  12260  infpnlem1  12311  mhmpropd  12689  grplcan  12761  txlm  13073  blininf  13218  xmeter  13230  xmetresbl  13234  limcimo  13428