Theorem 3ad2antr1 1188

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 479	. 2 |- ( ( ph /\ ( ch /\ ps ) ) -> th )
3	2	3adantr3 1184	1 |- ( ( ph /\ ( ch /\ ps /\ ta ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  ispod  4401  poxp  6397  fzosubel2  10441  hashdifpr  11085  pfxccat3a  11323  grpsubadd  13689  mulgnnass  13762  mulgnn0ass  13763  issubg2m  13794  srgdilem  14001  lsssn0  14403  dvconst  15437  dvconstre  15439  isclwwlk  16264  clwwlkccatlem  16270  clwwlkccat  16271