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  7448  ctssdclemn0  7457  cauappcvgprlemladdfu  8028  caucvgprlemloc  8049  caucvgprlemladdfu  8051  caucvgprlemlim  8055  caucvgprprlemml  8068  caucvgprprlemloc  8077  caucvgprprlemlim  8085  suplocexprlemmu  8092  suplocexprlemru  8093  suplocexprlemloc  8095  suplocsrlem  8182  axcaucvglemres  8273  nn0ltexp2  11170  resqrexlemglsq  11811  fiidxsupcl  12019  xrmaxifle  12038  xrmaxiflemlub  12040  divalglemeuneg  12716  bezoutlemnewy  12799  4sqlemsdc  13209  ctiunctlemfo  13389  mhmmnd  13979  psrbaglefifi  15177  txmetcnp  15756  mulcncf  15846  suplociccreex  15862  cnplimclemr  15907  limccnpcntop  15913  lgsval  16340