Theorem ad5antr 487

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 485	. 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  489  difinfinf  6986  ctssdclemn0  6995  cauappcvgprlemladdfu  7462  caucvgprlemloc  7483  caucvgprlemladdfu  7485  caucvgprlemlim  7489  caucvgprprlemml  7502  caucvgprprlemloc  7511  caucvgprprlemlim  7519  suplocexprlemmu  7526  suplocexprlemru  7527  suplocexprlemloc  7529  suplocsrlem  7616  axcaucvglemres  7707  resqrexlemglsq  10794  xrmaxifle  11015  xrmaxiflemlub  11017  divalglemeuneg  11620  bezoutlemnewy  11684  ctiunctlemfo  11952  txmetcnp  12687  mulcncf  12760  suplociccreex  12771  cnplimclemr  12807  limccnpcntop  12813