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  7118  ctssdclemn0  7127  cauappcvgprlemladdfu  7671  caucvgprlemloc  7692  caucvgprlemladdfu  7694  caucvgprlemlim  7698  caucvgprprlemml  7711  caucvgprprlemloc  7720  caucvgprprlemlim  7728  suplocexprlemmu  7735  suplocexprlemru  7736  suplocexprlemloc  7738  suplocsrlem  7825  axcaucvglemres  7916  nn0ltexp2  10707  resqrexlemglsq  11049  xrmaxifle  11272  xrmaxiflemlub  11274  divalglemeuneg  11946  bezoutlemnewy  12015  ctiunctlemfo  12458  mhmmnd  13024  txmetcnp  14415  mulcncf  14488  suplociccreex  14499  cnplimclemr  14535  limccnpcntop  14541  lgsval  14802