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  10630  hashdifpr  11283  pfxccat3a  11532  grpsubadd  13952  mulgnnass  14019  mulgnn0ass  14020  issubg2m  14051  srgdilem  14380  lsssn0  14816  dvconst  15920  dvconstre  15922  isclwwlk  16840  clwwlkccatlem  16846  clwwlkccat  16847