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  5570  fvun1  5712  isocnv  5952  isores2  5954  f1oiso2  5968  offval  6243  xp2nd  6329  1stconst  6386  2ndconst  6387  tfrlem9  6485  nnmordi  6684  dom2lem  6945  fundmen  6981  mapen  7032  ssenen  7037  ltsonq  7618  ltexnqq  7628  genprndl  7741  genprndu  7742  ltpopr  7815  ltsopr  7816  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemdisj  7826  ltexprlemfl  7829  ltexprlemfu  7831  mulcmpblnrlemg  7960  cnegexlem2  8355  muladd  8563  eqord1  8663  eqord2  8664  divadddivap  8907  ltmul12a  9040  lemul12b  9041  cju  9141  zextlt  9572  supinfneg  9829  infsupneg  9830  xrre  10055  ixxdisj  10138  iooshf  10187  icodisj  10227  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  iccf1o  10239  fzaddel  10294  fzsubel  10295  seq3caopr  10757  seqcaoprg  10758  expineg2  10810  expsubap  10849  expnbnd  10925  facndiv  11001  hashfacen  11100  ccatpfx  11282  swrdccatfn  11305  swrdccatin2  11310  fprodeq0  12179  lcmdvds  12652  hashdvds  12794  eulerthlemh  12804  pceu  12869  pcqcl  12880  infpnlem1  12933  4sqlem11  12975  mhmpropd  13550  subsubm  13567  grplcan  13646  grplmulf1o  13658  dfgrp3mlem  13682  mulgfng  13712  mulgsubcl  13724  subsubg  13785  eqger  13812  resghm  13848  conjghm  13864  subsubrng  14230  subsubrg  14261  psrgrp  14701  txlm  15005  blininf  15150  xmeter  15162  xmetresbl  15166  limcimo  15391  dvdsppwf1o  15715  fsumdvdsmul  15717  sgmmul  15722  clwwlkn1loopb  16273