Theorem 3ad2antr1 1193

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

Hypothesis

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

Assertion

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

Proof of Theorem 3ad2antr1

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 |- ( ( ph /\ ch ) -> th )
2	1	adantrr 483	. 2 |- ( ( ph /\ ( ch /\ ps ) ) -> th )
3	2	3adantr3 1189	1 |- ( ( ph /\ ( ch /\ ps /\ ta ) ) -> th )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ispod  4449  poxp  6468  fzosubel2  10623  hashdifpr  11275  pfxccat3a  11524  grpsubadd  13942  mulgnnass  14009  mulgnn0ass  14010  issubg2m  14041  srgdilem  14322  lsssn0  14756  dvconst  15844  dvconstre  15846  isclwwlk  16733  clwwlkccatlem  16739  clwwlkccat  16740