Theorem ad5antr 496

Description: Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad5antr	⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Proof of Theorem ad5antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	ad4antr 494	. 2 ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
3	2	adantr 276	1 ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

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  7276  ctssdclemn0  7285  cauappcvgprlemladdfu  7849  caucvgprlemloc  7870  caucvgprlemladdfu  7872  caucvgprlemlim  7876  caucvgprprlemml  7889  caucvgprprlemloc  7898  caucvgprprlemlim  7906  suplocexprlemmu  7913  suplocexprlemru  7914  suplocexprlemloc  7916  suplocsrlem  8003  axcaucvglemres  8094  nn0ltexp2  10939  resqrexlemglsq  11541  xrmaxifle  11765  xrmaxiflemlub  11767  divalglemeuneg  12442  bezoutlemnewy  12525  4sqlemsdc  12931  ctiunctlemfo  13018  mhmmnd  13661  txmetcnp  15200  mulcncf  15290  suplociccreex  15306  cnplimclemr  15351  limccnpcntop  15357  lgsval  15691