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  7176  ctssdclemn0  7185  cauappcvgprlemladdfu  7738  caucvgprlemloc  7759  caucvgprlemladdfu  7761  caucvgprlemlim  7765  caucvgprprlemml  7778  caucvgprprlemloc  7787  caucvgprprlemlim  7795  suplocexprlemmu  7802  suplocexprlemru  7803  suplocexprlemloc  7805  suplocsrlem  7892  axcaucvglemres  7983  nn0ltexp2  10818  resqrexlemglsq  11204  xrmaxifle  11428  xrmaxiflemlub  11430  divalglemeuneg  12105  bezoutlemnewy  12188  4sqlemsdc  12594  ctiunctlemfo  12681  mhmmnd  13322  txmetcnp  14838  mulcncf  14928  suplociccreex  14944  cnplimclemr  14989  limccnpcntop  14995  lgsval  15329