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  11168  resqrexlemglsq  11809  fiidxsupcl  12017  xrmaxifle  12036  xrmaxiflemlub  12038  divalglemeuneg  12714  bezoutlemnewy  12797  4sqlemsdc  13207  ctiunctlemfo  13387  mhmmnd  13977  psrbaglefifi  15175  psrbagmaxlem1  15178  mplsubgfilemcl  15232  txmetcnp  15761  mulcncf  15851  suplociccreex  15867  cnplimclemr  15912  limccnpcntop  15918  lgsval  16345