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 ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad6antr  502  difinfinf  7441  ctssdclemn0  7450  cauappcvgprlemladdfu  8021  caucvgprlemloc  8042  caucvgprlemladdfu  8044  caucvgprlemlim  8048  caucvgprprlemml  8061  caucvgprprlemloc  8070  caucvgprprlemlim  8078  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemloc  8088  suplocsrlem  8175  axcaucvglemres  8266  nn0ltexp2  11149  resqrexlemglsq  11790  xrmaxifle  12014  xrmaxiflemlub  12016  divalglemeuneg  12692  bezoutlemnewy  12775  4sqlemsdc  13181  ctiunctlemfo  13332  mhmmnd  13921  txmetcnp  15621  mulcncf  15711  suplociccreex  15727  cnplimclemr  15772  limccnpcntop  15778  lgsval  16135