Theorem ad5antr 500

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 498	. 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  502  difinfinf  7431  ctssdclemn0  7440  cauappcvgprlemladdfu  8011  caucvgprlemloc  8032  caucvgprlemladdfu  8034  caucvgprlemlim  8038  caucvgprprlemml  8051  caucvgprprlemloc  8060  caucvgprprlemlim  8068  suplocexprlemmu  8075  suplocexprlemru  8076  suplocexprlemloc  8078  suplocsrlem  8165  axcaucvglemres  8256  nn0ltexp2  11125  resqrexlemglsq  11766  xrmaxifle  11990  xrmaxiflemlub  11992  divalglemeuneg  12668  bezoutlemnewy  12751  4sqlemsdc  13157  ctiunctlemfo  13308  mhmmnd  13896  txmetcnp  15542  mulcncf  15632  suplociccreex  15648  cnplimclemr  15693  limccnpcntop  15699  lgsval  16037