Theorem 3ad2antr2 1147

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

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

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 960

This theorem is referenced by:  axdc4lem  8612  ioc0  11334  grpsubadd  15592  psrbaglesupp  17368  zntoslem  17830  trcfilu  19710  constr2wlk  23319  constr2trl  23320  constr3trllem1  23358  grpopnpcan2  23562  mdsl3  25542  dvrcan5  26113  brofs2  27954  brifs2  27955  ftc1anc  28316  frinfm  28470  welb  28471  fdc  28482  unichnidl  28672  ldepsprlem  30712  cvrnbtwn2  32490  islpln2a  32762  paddss1  33031  paddss2  33032  paddasslem17  33050  tendospass  34234