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  7442  ctssdclemn0  7451  cauappcvgprlemladdfu  8022  caucvgprlemloc  8043  caucvgprlemladdfu  8045  caucvgprlemlim  8049  caucvgprprlemml  8062  caucvgprprlemloc  8071  caucvgprprlemlim  8079  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemloc  8089  suplocsrlem  8176  axcaucvglemres  8267  nn0ltexp2  11163  resqrexlemglsq  11804  fiidxsupcl  12012  xrmaxifle  12031  xrmaxiflemlub  12033  divalglemeuneg  12709  bezoutlemnewy  12792  4sqlemsdc  13202  ctiunctlemfo  13382  mhmmnd  13972  psrbaglefifi  15147  txmetcnp  15710  mulcncf  15800  suplociccreex  15816  cnplimclemr  15861  limccnpcntop  15867  lgsval  16289