Theorem ad5antr 496

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

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  ad6antr  498  difinfinf  7343  ctssdclemn0  7352  cauappcvgprlemladdfu  7917  caucvgprlemloc  7938  caucvgprlemladdfu  7940  caucvgprlemlim  7944  caucvgprprlemml  7957  caucvgprprlemloc  7966  caucvgprprlemlim  7974  suplocexprlemmu  7981  suplocexprlemru  7982  suplocexprlemloc  7984  suplocsrlem  8071  axcaucvglemres  8162  nn0ltexp2  11017  resqrexlemglsq  11645  xrmaxifle  11869  xrmaxiflemlub  11871  divalglemeuneg  12547  bezoutlemnewy  12630  4sqlemsdc  13036  ctiunctlemfo  13123  mhmmnd  13766  txmetcnp  15312  mulcncf  15402  suplociccreex  15418  cnplimclemr  15463  limccnpcntop  15469  lgsval  15806