Theorem ad5antr 493

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  ad6antr  495  difinfinf  7078  ctssdclemn0  7087  cauappcvgprlemladdfu  7616  caucvgprlemloc  7637  caucvgprlemladdfu  7639  caucvgprlemlim  7643  caucvgprprlemml  7656  caucvgprprlemloc  7665  caucvgprprlemlim  7673  suplocexprlemmu  7680  suplocexprlemru  7681  suplocexprlemloc  7683  suplocsrlem  7770  axcaucvglemres  7861  nn0ltexp2  10644  resqrexlemglsq  10986  xrmaxifle  11209  xrmaxiflemlub  11211  divalglemeuneg  11882  bezoutlemnewy  11951  ctiunctlemfo  12394  txmetcnp  13312  mulcncf  13385  suplociccreex  13396  cnplimclemr  13432  limccnpcntop  13438  lgsval  13699