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  7279  ctssdclemn0  7288  cauappcvgprlemladdfu  7852  caucvgprlemloc  7873  caucvgprlemladdfu  7875  caucvgprlemlim  7879  caucvgprprlemml  7892  caucvgprprlemloc  7901  caucvgprprlemlim  7909  suplocexprlemmu  7916  suplocexprlemru  7917  suplocexprlemloc  7919  suplocsrlem  8006  axcaucvglemres  8097  nn0ltexp2  10943  resqrexlemglsq  11548  xrmaxifle  11772  xrmaxiflemlub  11774  divalglemeuneg  12449  bezoutlemnewy  12532  4sqlemsdc  12938  ctiunctlemfo  13025  mhmmnd  13668  txmetcnp  15207  mulcncf  15297  suplociccreex  15313  cnplimclemr  15358  limccnpcntop  15364  lgsval  15698