Theorem ad5antr 500

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 498	. 2 |- ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) -> ps )
3	2	adantr 276	1 |- ( ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) -> ps )

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:  ad6antr  502  difinfinf  7447  ctssdclemn0  7456  cauappcvgprlemladdfu  8027  caucvgprlemloc  8048  caucvgprlemladdfu  8050  caucvgprlemlim  8054  caucvgprprlemml  8067  caucvgprprlemloc  8076  caucvgprprlemlim  8084  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemloc  8094  suplocsrlem  8181  axcaucvglemres  8272  nn0ltexp2  11169  resqrexlemglsq  11810  fiidxsupcl  12018  xrmaxifle  12037  xrmaxiflemlub  12039  divalglemeuneg  12715  bezoutlemnewy  12798  4sqlemsdc  13208  ctiunctlemfo  13388  mhmmnd  13978  psrbaglefifi  15172  txmetcnp  15744  mulcncf  15834  suplociccreex  15850  cnplimclemr  15895  limccnpcntop  15901  lgsval  16328