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  1187  3ad2antr3  1188  xordidc  1441  foco  5561  fvun1  5702  isocnv  5941  isores2  5943  f1oiso2  5957  offval  6232  xp2nd  6318  1stconst  6373  2ndconst  6374  tfrlem9  6471  nnmordi  6670  dom2lem  6931  fundmen  6967  mapen  7015  ssenen  7020  ltsonq  7596  ltexnqq  7606  genprndl  7719  genprndu  7720  ltpopr  7793  ltsopr  7794  ltexprlemm  7798  ltexprlemopl  7799  ltexprlemopu  7801  ltexprlemdisj  7804  ltexprlemfl  7807  ltexprlemfu  7809  mulcmpblnrlemg  7938  cnegexlem2  8333  muladd  8541  eqord1  8641  eqord2  8642  divadddivap  8885  ltmul12a  9018  lemul12b  9019  cju  9119  zextlt  9550  supinfneg  9802  infsupneg  9803  xrre  10028  ixxdisj  10111  iooshf  10160  icodisj  10200  iccshftr  10202  iccshftl  10204  iccdil  10206  icccntr  10208  iccf1o  10212  fzaddel  10267  fzsubel  10268  seq3caopr  10729  seqcaoprg  10730  expineg2  10782  expsubap  10821  expnbnd  10897  facndiv  10973  hashfacen  11071  ccatpfx  11249  swrdccatfn  11272  swrdccatin2  11277  fprodeq0  12144  lcmdvds  12617  hashdvds  12759  eulerthlemh  12769  pceu  12834  pcqcl  12845  infpnlem1  12898  4sqlem11  12940  mhmpropd  13515  subsubm  13532  grplcan  13611  grplmulf1o  13623  dfgrp3mlem  13647  mulgfng  13677  mulgsubcl  13689  subsubg  13750  eqger  13777  resghm  13813  conjghm  13829  subsubrng  14194  subsubrg  14225  psrgrp  14665  txlm  14969  blininf  15114  xmeter  15126  xmetresbl  15130  limcimo  15355  dvdsppwf1o  15679  fsumdvdsmul  15681  sgmmul  15686  clwwlkn1loopb  16162