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  6994  ctssdclemn0  7003  cauappcvgprlemladdfu  7486  caucvgprlemloc  7507  caucvgprlemladdfu  7509  caucvgprlemlim  7513  caucvgprprlemml  7526  caucvgprprlemloc  7535  caucvgprprlemlim  7543  suplocexprlemmu  7550  suplocexprlemru  7551  suplocexprlemloc  7553  suplocsrlem  7640  axcaucvglemres  7731  resqrexlemglsq  10826  xrmaxifle  11047  xrmaxiflemlub  11049  divalglemeuneg  11656  bezoutlemnewy  11720  ctiunctlemfo  11988  txmetcnp  12726  mulcncf  12799  suplociccreex  12810  cnplimclemr  12846  limccnpcntop  12852