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  4451  poxp  6472  fzosubel2  10629  hashdifpr  11282  pfxccat3a  11531  grpsubadd  13951  mulgnnass  14018  mulgnn0ass  14019  issubg2m  14050  srgdilem  14379  lsssn0  14815  dvconst  15937  dvconstre  15939  isclwwlk  16857  clwwlkccatlem  16863  clwwlkccat  16864