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  7236  ctssdclemn0  7245  cauappcvgprlemladdfu  7809  caucvgprlemloc  7830  caucvgprlemladdfu  7832  caucvgprlemlim  7836  caucvgprprlemml  7849  caucvgprprlemloc  7858  caucvgprprlemlim  7866  suplocexprlemmu  7873  suplocexprlemru  7874  suplocexprlemloc  7876  suplocsrlem  7963  axcaucvglemres  8054  nn0ltexp2  10898  resqrexlemglsq  11499  xrmaxifle  11723  xrmaxiflemlub  11725  divalglemeuneg  12400  bezoutlemnewy  12483  4sqlemsdc  12889  ctiunctlemfo  12976  mhmmnd  13619  txmetcnp  15157  mulcncf  15247  suplociccreex  15263  cnplimclemr  15308  limccnpcntop  15314  lgsval  15648