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  10613  hashdifpr  11261  pfxccat3a  11510  grpsubadd  13893  mulgnnass  13960  mulgnn0ass  13961  issubg2m  13992  srgdilem  14273  lsssn0  14707  dvconst  15795  dvconstre  15797  isclwwlk  16635  clwwlkccatlem  16641  clwwlkccat  16642