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  7392  ctssdclemn0  7401  cauappcvgprlemladdfu  7969  caucvgprlemloc  7990  caucvgprlemladdfu  7992  caucvgprlemlim  7996  caucvgprprlemml  8009  caucvgprprlemloc  8018  caucvgprprlemlim  8026  suplocexprlemmu  8033  suplocexprlemru  8034  suplocexprlemloc  8036  suplocsrlem  8123  axcaucvglemres  8214  nn0ltexp2  11071  resqrexlemglsq  11707  xrmaxifle  11931  xrmaxiflemlub  11933  divalglemeuneg  12609  bezoutlemnewy  12692  4sqlemsdc  13098  ctiunctlemfo  13190  mhmmnd  13833  txmetcnp  15383  mulcncf  15473  suplociccreex  15489  cnplimclemr  15534  limccnpcntop  15540  lgsval  15877