Theorem 3adantr3 1184

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

Proof of Theorem 3adantr3

Step	Hyp	Ref	Expression
1		3simpa 1020	. 2 |- ( ( ps /\ ch /\ ta ) -> ( ps /\ ch ) )
2		3adantr.1	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	1, 2	sylan2 286	1 |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  3ad2antr1  1188  3ad2antr2  1189  3adant3r3  1240  isosolem  5965  caovlem2d  6215  swrdspsleq  11252  tanaddap  12318  prdssgrpd  13516  prdsmndd  13549  mhmmnd  13721  imasrng  13988  imasring  14096  isxmet2d  15091  xmetres2  15122  comet  15242  xmetxp  15250  iswlkg  16199