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  7299  ctssdclemn0  7308  cauappcvgprlemladdfu  7873  caucvgprlemloc  7894  caucvgprlemladdfu  7896  caucvgprlemlim  7900  caucvgprprlemml  7913  caucvgprprlemloc  7922  caucvgprprlemlim  7930  suplocexprlemmu  7937  suplocexprlemru  7938  suplocexprlemloc  7940  suplocsrlem  8027  axcaucvglemres  8118  nn0ltexp2  10970  resqrexlemglsq  11582  xrmaxifle  11806  xrmaxiflemlub  11808  divalglemeuneg  12483  bezoutlemnewy  12566  4sqlemsdc  12972  ctiunctlemfo  13059  mhmmnd  13702  txmetcnp  15241  mulcncf  15331  suplociccreex  15347  cnplimclemr  15392  limccnpcntop  15398  lgsval  15732