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  7160  ctssdclemn0  7169  cauappcvgprlemladdfu  7714  caucvgprlemloc  7735  caucvgprlemladdfu  7737  caucvgprlemlim  7741  caucvgprprlemml  7754  caucvgprprlemloc  7763  caucvgprprlemlim  7771  suplocexprlemmu  7778  suplocexprlemru  7779  suplocexprlemloc  7781  suplocsrlem  7868  axcaucvglemres  7959  nn0ltexp2  10780  resqrexlemglsq  11166  xrmaxifle  11389  xrmaxiflemlub  11391  divalglemeuneg  12064  bezoutlemnewy  12133  4sqlemsdc  12538  ctiunctlemfo  12596  mhmmnd  13186  txmetcnp  14686  mulcncf  14762  suplociccreex  14778  cnplimclemr  14823  limccnpcntop  14829  lgsval  15120