Theorem 3ad2antr2 1196

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

Hypothesis

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

Assertion

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

Proof of Theorem 3ad2antr2

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 |- ( ( ph /\ ch ) -> th )
2	1	adantrl 730	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	2	3adantr3 1191	1 |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 376   /\ w3a 1007

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 190  df-an 378  df-3an 1009

This theorem is referenced by:  axdc4lem  8903  ioc0  11708  funcestrcsetclem9  16111  funcsetcestrclem9  16126  grpsubadd  16820  psrbaglesupp  18669  zntoslem  19204  trcfilu  21387  constr2wlk  25407  constr2trl  25408  constr3trllem1  25457  grpopnpcan2  26062  mdsl3  28050  dvrcan5  28630  brofs2  30915  brifs2  30916  poimirlem28  32032  ftc1anc  32089  frinfm  32126  welb  32127  fdc  32138  unichnidl  32328  cvrnbtwn2  32912  islpln2a  33184  paddss1  33453  paddss2  33454  paddasslem17  33472  tendospass  34658  funcringcsetcALTV2lem9  40554  funcringcsetclem9ALTV  40577  ldepsprlem  40773