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  1163  3ad2antr3  1164  xordidc  1399  foco  5440  fvun1  5574  isocnv  5802  isores2  5804  f1oiso2  5818  offval  6080  xp2nd  6157  1stconst  6212  2ndconst  6213  tfrlem9  6310  nnmordi  6507  dom2lem  6762  fundmen  6796  mapen  6836  ssenen  6841  ltsonq  7372  ltexnqq  7382  genprndl  7495  genprndu  7496  ltpopr  7569  ltsopr  7570  ltexprlemm  7574  ltexprlemopl  7575  ltexprlemopu  7577  ltexprlemdisj  7580  ltexprlemfl  7583  ltexprlemfu  7585  mulcmpblnrlemg  7714  cnegexlem2  8107  muladd  8315  eqord1  8414  eqord2  8415  divadddivap  8657  ltmul12a  8790  lemul12b  8791  cju  8891  zextlt  9318  supinfneg  9568  infsupneg  9569  xrre  9791  ixxdisj  9874  iooshf  9923  icodisj  9963  iccshftr  9965  iccshftl  9967  iccdil  9969  icccntr  9971  iccf1o  9975  fzaddel  10029  fzsubel  10030  seq3caopr  10453  expineg2  10499  expsubap  10538  expnbnd  10613  facndiv  10687  hashfacen  10784  fprodeq0  11593  lcmdvds  12046  hashdvds  12188  eulerthlemh  12198  pceu  12262  pcqcl  12273  infpnlem1  12324  mhmpropd  12720  grplcan  12793  grplmulf1o  12805  dfgrp3mlem  12829  mulgfng  12848  mulgsubcl  12858  txlm  13350  blininf  13495  xmeter  13507  xmetresbl  13511  limcimo  13705