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  1165  3ad2antr3  1166  xordidc  1410  foco  5467  fvun1  5603  isocnv  5833  isores2  5835  f1oiso2  5849  offval  6114  xp2nd  6191  1stconst  6246  2ndconst  6247  tfrlem9  6344  nnmordi  6541  dom2lem  6798  fundmen  6832  mapen  6874  ssenen  6879  ltsonq  7427  ltexnqq  7437  genprndl  7550  genprndu  7551  ltpopr  7624  ltsopr  7625  ltexprlemm  7629  ltexprlemopl  7630  ltexprlemopu  7632  ltexprlemdisj  7635  ltexprlemfl  7638  ltexprlemfu  7640  mulcmpblnrlemg  7769  cnegexlem2  8163  muladd  8371  eqord1  8470  eqord2  8471  divadddivap  8714  ltmul12a  8847  lemul12b  8848  cju  8948  zextlt  9375  supinfneg  9625  infsupneg  9626  xrre  9850  ixxdisj  9933  iooshf  9982  icodisj  10022  iccshftr  10024  iccshftl  10026  iccdil  10028  icccntr  10030  iccf1o  10034  fzaddel  10089  fzsubel  10090  seq3caopr  10514  expineg2  10560  expsubap  10599  expnbnd  10675  facndiv  10751  hashfacen  10848  fprodeq0  11657  lcmdvds  12111  hashdvds  12253  eulerthlemh  12263  pceu  12327  pcqcl  12338  infpnlem1  12391  4sqlem11  12433  mhmpropd  12918  subsubm  12935  grplcan  13006  grplmulf1o  13018  dfgrp3mlem  13042  mulgfng  13066  mulgsubcl  13076  subsubg  13136  eqger  13163  resghm  13199  conjghm  13215  subsubrng  13561  subsubrg  13592  txlm  14236  blininf  14381  xmeter  14393  xmetresbl  14397  limcimo  14591