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  5509  fvun1  5645  isocnv  5880  isores2  5882  f1oiso2  5896  offval  6166  xp2nd  6252  1stconst  6307  2ndconst  6308  tfrlem9  6405  nnmordi  6602  dom2lem  6863  fundmen  6898  mapen  6943  ssenen  6948  ltsonq  7511  ltexnqq  7521  genprndl  7634  genprndu  7635  ltpopr  7708  ltsopr  7709  ltexprlemm  7713  ltexprlemopl  7714  ltexprlemopu  7716  ltexprlemdisj  7719  ltexprlemfl  7722  ltexprlemfu  7724  mulcmpblnrlemg  7853  cnegexlem2  8248  muladd  8456  eqord1  8556  eqord2  8557  divadddivap  8800  ltmul12a  8933  lemul12b  8934  cju  9034  zextlt  9465  supinfneg  9716  infsupneg  9717  xrre  9942  ixxdisj  10025  iooshf  10074  icodisj  10114  iccshftr  10116  iccshftl  10118  iccdil  10120  icccntr  10122  iccf1o  10126  fzaddel  10181  fzsubel  10182  seq3caopr  10640  seqcaoprg  10641  expineg2  10693  expsubap  10732  expnbnd  10808  facndiv  10884  hashfacen  10981  fprodeq0  11928  lcmdvds  12401  hashdvds  12543  eulerthlemh  12553  pceu  12618  pcqcl  12629  infpnlem1  12682  4sqlem11  12724  mhmpropd  13298  subsubm  13315  grplcan  13394  grplmulf1o  13406  dfgrp3mlem  13430  mulgfng  13460  mulgsubcl  13472  subsubg  13533  eqger  13560  resghm  13596  conjghm  13612  subsubrng  13976  subsubrg  14007  psrgrp  14447  txlm  14751  blininf  14896  xmeter  14908  xmetresbl  14912  limcimo  15137  dvdsppwf1o  15461  fsumdvdsmul  15463  sgmmul  15468