Theorem 3ad2antr2 1154

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 715	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	2	3adantr3 1149	1 |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 965

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 185  df-an 371  df-3an 967

This theorem is referenced by:  axdc4lem  8645  ioc0  11368  grpsubadd  15634  psrbaglesupp  17457  zntoslem  18011  trcfilu  19891  constr2wlk  23519  constr2trl  23520  constr3trllem1  23558  grpopnpcan2  23762  mdsl3  25742  dvrcan5  26283  brofs2  28130  brifs2  28131  ftc1anc  28501  frinfm  28655  welb  28656  fdc  28667  unichnidl  28857  ldepsprlem  31003  cvrnbtwn2  33016  islpln2a  33288  paddss1  33557  paddss2  33558  paddasslem17  33576  tendospass  34760