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  5449  fvun1  5583  isocnv  5812  isores2  5814  f1oiso2  5828  offval  6090  xp2nd  6167  1stconst  6222  2ndconst  6223  tfrlem9  6320  nnmordi  6517  dom2lem  6772  fundmen  6806  mapen  6846  ssenen  6851  ltsonq  7397  ltexnqq  7407  genprndl  7520  genprndu  7521  ltpopr  7594  ltsopr  7595  ltexprlemm  7599  ltexprlemopl  7600  ltexprlemopu  7602  ltexprlemdisj  7605  ltexprlemfl  7608  ltexprlemfu  7610  mulcmpblnrlemg  7739  cnegexlem2  8133  muladd  8341  eqord1  8440  eqord2  8441  divadddivap  8684  ltmul12a  8817  lemul12b  8818  cju  8918  zextlt  9345  supinfneg  9595  infsupneg  9596  xrre  9820  ixxdisj  9903  iooshf  9952  icodisj  9992  iccshftr  9994  iccshftl  9996  iccdil  9998  icccntr  10000  iccf1o  10004  fzaddel  10059  fzsubel  10060  seq3caopr  10483  expineg2  10529  expsubap  10568  expnbnd  10644  facndiv  10719  hashfacen  10816  fprodeq0  11625  lcmdvds  12079  hashdvds  12221  eulerthlemh  12231  pceu  12295  pcqcl  12306  infpnlem1  12357  mhmpropd  12857  grplcan  12932  grplmulf1o  12944  dfgrp3mlem  12968  mulgfng  12987  mulgsubcl  12997  subsubg  13057  eqger  13083  subsubrg  13366  txlm  13782  blininf  13927  xmeter  13939  xmetresbl  13943  limcimo  14137