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  7100  ctssdclemn0  7109  cauappcvgprlemladdfu  7653  caucvgprlemloc  7674  caucvgprlemladdfu  7676  caucvgprlemlim  7680  caucvgprprlemml  7693  caucvgprprlemloc  7702  caucvgprprlemlim  7710  suplocexprlemmu  7717  suplocexprlemru  7718  suplocexprlemloc  7720  suplocsrlem  7807  axcaucvglemres  7898  nn0ltexp2  10689  resqrexlemglsq  11031  xrmaxifle  11254  xrmaxiflemlub  11256  divalglemeuneg  11928  bezoutlemnewy  11997  ctiunctlemfo  12440  mhmmnd  12980  txmetcnp  14021  mulcncf  14094  suplociccreex  14105  cnplimclemr  14141  limccnpcntop  14147  lgsval  14408