Theorem 3ad2antr2 1162

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 1157	1 |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )

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

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 975

This theorem is referenced by:  axdc4lem  8847  ioc0  11588  grpsubadd  15998  psrbaglesupp  17887  zntoslem  18464  trcfilu  20665  constr2wlk  24423  constr2trl  24424  constr3trllem1  24473  grpopnpcan2  25078  mdsl3  27058  dvrcan5  27608  brofs2  29654  brifs2  29655  ftc1anc  30025  frinfm  30153  welb  30154  fdc  30165  unichnidl  30355  funcringcsetclem9  32384  ldepsprlem  32555  cvrnbtwn2  34473  islpln2a  34745  paddss1  35014  paddss2  35015  paddasslem17  35033  tendospass  36217