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  7176  ctssdclemn0  7185  cauappcvgprlemladdfu  7740  caucvgprlemloc  7761  caucvgprlemladdfu  7763  caucvgprlemlim  7767  caucvgprprlemml  7780  caucvgprprlemloc  7789  caucvgprprlemlim  7797  suplocexprlemmu  7804  suplocexprlemru  7805  suplocexprlemloc  7807  suplocsrlem  7894  axcaucvglemres  7985  nn0ltexp2  10820  resqrexlemglsq  11206  xrmaxifle  11430  xrmaxiflemlub  11432  divalglemeuneg  12107  bezoutlemnewy  12190  4sqlemsdc  12596  ctiunctlemfo  12683  mhmmnd  13324  txmetcnp  14862  mulcncf  14952  suplociccreex  14968  cnplimclemr  15013  limccnpcntop  15019  lgsval  15353