Theorem 3ad2antr1 1226

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.)

Hypothesis

Ref	Expression
3ad2antl.1	|- ( ( ph /\ ch ) -> th )

Assertion

Ref	Expression
3ad2antr1	|- ( ( ph /\ ( ch /\ ps /\ ta ) ) -> th )

Proof of Theorem 3ad2antr1

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 |- ( ( ph /\ ch ) -> th )
2	1	adantrr 753	. 2 |- ( ( ph /\ ( ch /\ ps ) ) -> th )
3	2	3adantr3 1222	1 |- ( ( ph /\ ( ch /\ ps /\ ta ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  ispod  5043  funcnvqp  5952  dfwe2  6981  poxp  7289  cfcoflem  9094  axdc3lem  9272  fzadd2  12376  fzosubel2  12527  hashdifpr  13203  sqr0lem  13981  iscatd2  16342  funcestrcsetclem9  16788  funcsetcestrclem9  16803  curf2cl  16871  yonedalem4c  16917  grpsubadd  17503  mulgnnass  17576  mulgnnassOLD  17577  mulgnn0ass  17578  dprdss  18428  dprd2da  18441  srgi  18511  lsssn0  18948  psrbaglesupp  19368  zntoslem  19905  blsscls  22312  iimulcl  22736  pi1grplem  22849  pi1xfrf  22853  dvconst  23680  logexprlim  24950  wwlksnextbi  26789  umgr3cyclex  27043  nvss  27448  disjdsct  29480  issgon  30186  measdivcstOLD  30287  measdivcst  30288  elmrsubrn  31417  poimirlem28  33437  ftc1anc  33493  fdc  33541  cvrnbtwn3  34563  paddasslem9  35114  paddasslem17  35122  pmapjlln1  35141  lautj  35379  lautm  35380  dfsalgen2  40559  smflimlem4  40982  pfxccat3a  41429  splvalpfx  41435  lidldomnnring  41930  funcringcsetcALTV2lem9  42044  funcringcsetclem9ALTV  42067  lincresunit3lem2  42269