Theorem ad5antr 500

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 498	. 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  502  difinfinf  7435  ctssdclemn0  7444  cauappcvgprlemladdfu  8015  caucvgprlemloc  8036  caucvgprlemladdfu  8038  caucvgprlemlim  8042  caucvgprprlemml  8055  caucvgprprlemloc  8064  caucvgprprlemlim  8072  suplocexprlemmu  8079  suplocexprlemru  8080  suplocexprlemloc  8082  suplocsrlem  8169  axcaucvglemres  8260  nn0ltexp2  11130  resqrexlemglsq  11771  xrmaxifle  11995  xrmaxiflemlub  11997  divalglemeuneg  12673  bezoutlemnewy  12756  4sqlemsdc  13162  ctiunctlemfo  13313  mhmmnd  13902  txmetcnp  15602  mulcncf  15692  suplociccreex  15708  cnplimclemr  15753  limccnpcntop  15759  lgsval  16106