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  7264  ctssdclemn0  7273  cauappcvgprlemladdfu  7837  caucvgprlemloc  7858  caucvgprlemladdfu  7860  caucvgprlemlim  7864  caucvgprprlemml  7877  caucvgprprlemloc  7886  caucvgprprlemlim  7894  suplocexprlemmu  7901  suplocexprlemru  7902  suplocexprlemloc  7904  suplocsrlem  7991  axcaucvglemres  8082  nn0ltexp2  10926  resqrexlemglsq  11528  xrmaxifle  11752  xrmaxiflemlub  11754  divalglemeuneg  12429  bezoutlemnewy  12512  4sqlemsdc  12918  ctiunctlemfo  13005  mhmmnd  13648  txmetcnp  15186  mulcncf  15276  suplociccreex  15292  cnplimclemr  15337  limccnpcntop  15343  lgsval  15677