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  7162  ctssdclemn0  7171  cauappcvgprlemladdfu  7716  caucvgprlemloc  7737  caucvgprlemladdfu  7739  caucvgprlemlim  7743  caucvgprprlemml  7756  caucvgprprlemloc  7765  caucvgprprlemlim  7773  suplocexprlemmu  7780  suplocexprlemru  7781  suplocexprlemloc  7783  suplocsrlem  7870  axcaucvglemres  7961  nn0ltexp2  10783  resqrexlemglsq  11169  xrmaxifle  11392  xrmaxiflemlub  11394  divalglemeuneg  12067  bezoutlemnewy  12136  4sqlemsdc  12541  ctiunctlemfo  12599  mhmmnd  13189  txmetcnp  14697  mulcncf  14787  suplociccreex  14803  cnplimclemr  14848  limccnpcntop  14854  lgsval  15161