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  7203  ctssdclemn0  7212  cauappcvgprlemladdfu  7767  caucvgprlemloc  7788  caucvgprlemladdfu  7790  caucvgprlemlim  7794  caucvgprprlemml  7807  caucvgprprlemloc  7816  caucvgprprlemlim  7824  suplocexprlemmu  7831  suplocexprlemru  7832  suplocexprlemloc  7834  suplocsrlem  7921  axcaucvglemres  8012  nn0ltexp2  10854  resqrexlemglsq  11333  xrmaxifle  11557  xrmaxiflemlub  11559  divalglemeuneg  12234  bezoutlemnewy  12317  4sqlemsdc  12723  ctiunctlemfo  12810  mhmmnd  13452  txmetcnp  14990  mulcncf  15080  suplociccreex  15096  cnplimclemr  15141  limccnpcntop  15147  lgsval  15481