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  10624  hashdifpr  11277  pfxccat3a  11526  grpsubadd  13946  mulgnnass  14013  mulgnn0ass  14014  issubg2m  14045  srgdilem  14357  lsssn0  14791  dvconst  15886  dvconstre  15888  isclwwlk  16801  clwwlkccatlem  16807  clwwlkccat  16808