Theorem ad4ant14 518

Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)

Hypothesis

Ref	Expression
ad4ant2.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
ad4ant14	|- ( ( ( ( ph /\ th ) /\ ta ) /\ ps ) -> ch )

Proof of Theorem ad4ant14

Step	Hyp	Ref	Expression
1		ad4ant2.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	adantlr 481	. 2 |- ( ( ( ph /\ th ) /\ ps ) -> ch )
3	2	adantlr 481	1 |- ( ( ( ( ph /\ th ) /\ ta ) /\ ps ) -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad5ant15  525  ad5ant25  528  seqfeq4g  10989  prodmodclem2  12369  prodmodc  12370  zproddc  12371  fprod2d  12415  gcdsupex  12759  gcdsupcl  12760  grpinvalem  13764  gzsumwsubmcl  13860  gzsumwmhm  13862  gsum2dfilem2  14272  subrngintm  14629  plyco  16018  gausslemma2dlem1f1o  16417