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  11147  resqrexlemglsq  11788  xrmaxifle  12012  xrmaxiflemlub  12014  divalglemeuneg  12690  bezoutlemnewy  12773  4sqlemsdc  13179  ctiunctlemfo  13330  mhmmnd  13919  txmetcnp  15619  mulcncf  15709  suplociccreex  15725  cnplimclemr  15770  limccnpcntop  15776  lgsval  16123