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  7441  ctssdclemn0  7450  cauappcvgprlemladdfu  8021  caucvgprlemloc  8042  caucvgprlemladdfu  8044  caucvgprlemlim  8048  caucvgprprlemml  8061  caucvgprprlemloc  8070  caucvgprprlemlim  8078  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemloc  8088  suplocsrlem  8175  axcaucvglemres  8266  nn0ltexp2  11161  resqrexlemglsq  11802  xrmaxifle  12028  xrmaxiflemlub  12030  divalglemeuneg  12706  bezoutlemnewy  12789  4sqlemsdc  13199  ctiunctlemfo  13379  mhmmnd  13968  txmetcnp  15668  mulcncf  15758  suplociccreex  15774  cnplimclemr  15819  limccnpcntop  15825  lgsval  16221