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  7405  ctssdclemn0  7414  cauappcvgprlemladdfu  7985  caucvgprlemloc  8006  caucvgprlemladdfu  8008  caucvgprlemlim  8012  caucvgprprlemml  8025  caucvgprprlemloc  8034  caucvgprprlemlim  8042  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemloc  8052  suplocsrlem  8139  axcaucvglemres  8230  nn0ltexp2  11099  resqrexlemglsq  11735  xrmaxifle  11959  xrmaxiflemlub  11961  divalglemeuneg  12637  bezoutlemnewy  12720  4sqlemsdc  13126  ctiunctlemfo  13277  mhmmnd  13872  txmetcnp  15512  mulcncf  15602  suplociccreex  15618  cnplimclemr  15663  limccnpcntop  15669  lgsval  16006