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  7202  ctssdclemn0  7211  cauappcvgprlemladdfu  7766  caucvgprlemloc  7787  caucvgprlemladdfu  7789  caucvgprlemlim  7793  caucvgprprlemml  7806  caucvgprprlemloc  7815  caucvgprprlemlim  7823  suplocexprlemmu  7830  suplocexprlemru  7831  suplocexprlemloc  7833  suplocsrlem  7920  axcaucvglemres  8011  nn0ltexp2  10852  resqrexlemglsq  11304  xrmaxifle  11528  xrmaxiflemlub  11530  divalglemeuneg  12205  bezoutlemnewy  12288  4sqlemsdc  12694  ctiunctlemfo  12781  mhmmnd  13423  txmetcnp  14961  mulcncf  15051  suplociccreex  15067  cnplimclemr  15112  limccnpcntop  15118  lgsval  15452