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  7291  ctssdclemn0  7300  cauappcvgprlemladdfu  7864  caucvgprlemloc  7885  caucvgprlemladdfu  7887  caucvgprlemlim  7891  caucvgprprlemml  7904  caucvgprprlemloc  7913  caucvgprprlemlim  7921  suplocexprlemmu  7928  suplocexprlemru  7929  suplocexprlemloc  7931  suplocsrlem  8018  axcaucvglemres  8109  nn0ltexp2  10961  resqrexlemglsq  11573  xrmaxifle  11797  xrmaxiflemlub  11799  divalglemeuneg  12474  bezoutlemnewy  12557  4sqlemsdc  12963  ctiunctlemfo  13050  mhmmnd  13693  txmetcnp  15232  mulcncf  15322  suplociccreex  15338  cnplimclemr  15383  limccnpcntop  15389  lgsval  15723