Theorem ad5antr 487

Description: Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)

Hypothesis

Ref	Expression
ad2ant.1	|- ( ph -> ps )

Assertion

Ref	Expression
ad5antr	|- ( ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ps )

Proof of Theorem ad5antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	ad4antr 485	. 2 |- ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) -> ps )
3	2	adantr 274	1 |- ( ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  ad6antr  489  difinfinf  6979  ctssdclemn0  6988  cauappcvgprlemladdfu  7455  caucvgprlemloc  7476  caucvgprlemladdfu  7478  caucvgprlemlim  7482  caucvgprprlemml  7495  caucvgprprlemloc  7504  caucvgprprlemlim  7512  suplocexprlemmu  7519  suplocexprlemru  7520  suplocexprlemloc  7522  suplocsrlem  7609  axcaucvglemres  7700  resqrexlemglsq  10787  xrmaxifle  11008  xrmaxiflemlub  11010  divalglemeuneg  11609  bezoutlemnewy  11673  ctiunctlemfo  11941  txmetcnp  12676  mulcncf  12749  suplociccreex  12760  cnplimclemr  12796  limccnpcntop  12802