Theorem ad5antr 488

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 486	. 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  490  difinfinf  7062  ctssdclemn0  7071  cauappcvgprlemladdfu  7591  caucvgprlemloc  7612  caucvgprlemladdfu  7614  caucvgprlemlim  7618  caucvgprprlemml  7631  caucvgprprlemloc  7640  caucvgprprlemlim  7648  suplocexprlemmu  7655  suplocexprlemru  7656  suplocexprlemloc  7658  suplocsrlem  7745  axcaucvglemres  7836  nn0ltexp2  10619  resqrexlemglsq  10960  xrmaxifle  11183  xrmaxiflemlub  11185  divalglemeuneg  11856  bezoutlemnewy  11925  ctiunctlemfo  12368  txmetcnp  13118  mulcncf  13191  suplociccreex  13202  cnplimclemr  13238  limccnpcntop  13244  lgsval  13505