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  1166  3ad2antr3  1167  xordidc  1419  foco  5531  fvun1  5668  isocnv  5903  isores2  5905  f1oiso2  5919  offval  6189  xp2nd  6275  1stconst  6330  2ndconst  6331  tfrlem9  6428  nnmordi  6625  dom2lem  6886  fundmen  6922  mapen  6968  ssenen  6973  ltsonq  7546  ltexnqq  7556  genprndl  7669  genprndu  7670  ltpopr  7743  ltsopr  7744  ltexprlemm  7748  ltexprlemopl  7749  ltexprlemopu  7751  ltexprlemdisj  7754  ltexprlemfl  7757  ltexprlemfu  7759  mulcmpblnrlemg  7888  cnegexlem2  8283  muladd  8491  eqord1  8591  eqord2  8592  divadddivap  8835  ltmul12a  8968  lemul12b  8969  cju  9069  zextlt  9500  supinfneg  9751  infsupneg  9752  xrre  9977  ixxdisj  10060  iooshf  10109  icodisj  10149  iccshftr  10151  iccshftl  10153  iccdil  10155  icccntr  10157  iccf1o  10161  fzaddel  10216  fzsubel  10217  seq3caopr  10677  seqcaoprg  10678  expineg2  10730  expsubap  10769  expnbnd  10845  facndiv  10921  hashfacen  11018  ccatpfx  11192  swrdccatfn  11215  swrdccatin2  11220  fprodeq0  12043  lcmdvds  12516  hashdvds  12658  eulerthlemh  12668  pceu  12733  pcqcl  12744  infpnlem1  12797  4sqlem11  12839  mhmpropd  13413  subsubm  13430  grplcan  13509  grplmulf1o  13521  dfgrp3mlem  13545  mulgfng  13575  mulgsubcl  13587  subsubg  13648  eqger  13675  resghm  13711  conjghm  13727  subsubrng  14091  subsubrg  14122  psrgrp  14562  txlm  14866  blininf  15011  xmeter  15023  xmetresbl  15027  limcimo  15252  dvdsppwf1o  15576  fsumdvdsmul  15578  sgmmul  15583