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  7095  ctssdclemn0  7104  cauappcvgprlemladdfu  7648  caucvgprlemloc  7669  caucvgprlemladdfu  7671  caucvgprlemlim  7675  caucvgprprlemml  7688  caucvgprprlemloc  7697  caucvgprprlemlim  7705  suplocexprlemmu  7712  suplocexprlemru  7713  suplocexprlemloc  7715  suplocsrlem  7802  axcaucvglemres  7893  nn0ltexp2  10681  resqrexlemglsq  11022  xrmaxifle  11245  xrmaxiflemlub  11247  divalglemeuneg  11918  bezoutlemnewy  11987  ctiunctlemfo  12430  mhmmnd  12908  txmetcnp  13800  mulcncf  13873  suplociccreex  13884  cnplimclemr  13920  limccnpcntop  13926  lgsval  14187