Theorem adantrl 469

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  499  ad2ant2rl  502  3ad2antr2  1147  3ad2antr3  1148  xordidc  1377  foco  5350  fvun1  5480  isocnv  5705  isores2  5707  f1oiso2  5721  offval  5982  xp2nd  6057  1stconst  6111  2ndconst  6112  tfrlem9  6209  nnmordi  6405  dom2lem  6659  fundmen  6693  mapen  6733  ssenen  6738  ltsonq  7199  ltexnqq  7209  genprndl  7322  genprndu  7323  ltpopr  7396  ltsopr  7397  ltexprlemm  7401  ltexprlemopl  7402  ltexprlemopu  7404  ltexprlemdisj  7407  ltexprlemfl  7410  ltexprlemfu  7412  mulcmpblnrlemg  7541  cnegexlem2  7931  muladd  8139  eqord1  8238  eqord2  8239  divadddivap  8480  ltmul12a  8611  lemul12b  8612  cju  8712  zextlt  9136  supinfneg  9383  infsupneg  9384  xrre  9596  ixxdisj  9679  iooshf  9728  icodisj  9768  iccshftr  9770  iccshftl  9772  iccdil  9774  icccntr  9776  iccf1o  9780  fzaddel  9832  fzsubel  9833  seq3caopr  10249  expineg2  10295  expsubap  10334  expnbnd  10408  facndiv  10478  hashfacen  10572  lcmdvds  11749  hashdvds  11886  txlm  12437  blininf  12582  xmeter  12594  xmetresbl  12598  limcimo  12792