Theorem 3adantr2 1221

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)

Hypothesis

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

Assertion

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

Proof of Theorem 3adantr2

Step	Hyp	Ref	Expression
1		3simpb 1059	. 2 |- ( ( ps /\ ta /\ ch ) -> ( ps /\ ch ) )
2		3adantr.1	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	1, 2	sylan2 491	1 |- ( ( ph /\ ( ps /\ ta /\ ch ) ) -> 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:  3adant3r2  1275  po3nr  5049  funcnvqp  5952  sornom  9099  axdclem2  9342  fzadd2  12376  issubc3  16509  funcestrcsetclem9  16788  funcsetcestrclem9  16803  pgpfi  18020  imasring  18619  prdslmodd  18969  icoopnst  22738  iocopnst  22739  axcontlem4  25847  nvmdi  27503  mdsl3  29175  elicc3  32311  iscringd  33797  erngdvlem3  36278  erngdvlem3-rN  36286  dvalveclem  36314  dvhlveclem  36397  dvmptfprodlem  40159  smflimlem4  40982  funcringcsetcALTV2lem9  42044  funcringcsetclem9ALTV  42067