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  7229  ctssdclemn0  7238  cauappcvgprlemladdfu  7802  caucvgprlemloc  7823  caucvgprlemladdfu  7825  caucvgprlemlim  7829  caucvgprprlemml  7842  caucvgprprlemloc  7851  caucvgprprlemlim  7859  suplocexprlemmu  7866  suplocexprlemru  7867  suplocexprlemloc  7869  suplocsrlem  7956  axcaucvglemres  8047  nn0ltexp2  10891  resqrexlemglsq  11448  xrmaxifle  11672  xrmaxiflemlub  11674  divalglemeuneg  12349  bezoutlemnewy  12432  4sqlemsdc  12838  ctiunctlemfo  12925  mhmmnd  13567  txmetcnp  15105  mulcncf  15195  suplociccreex  15211  cnplimclemr  15256  limccnpcntop  15262  lgsval  15596