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  7391  ctssdclemn0  7400  cauappcvgprlemladdfu  7965  caucvgprlemloc  7986  caucvgprlemladdfu  7988  caucvgprlemlim  7992  caucvgprprlemml  8005  caucvgprprlemloc  8014  caucvgprprlemlim  8022  suplocexprlemmu  8029  suplocexprlemru  8030  suplocexprlemloc  8032  suplocsrlem  8119  axcaucvglemres  8210  nn0ltexp2  11067  resqrexlemglsq  11700  xrmaxifle  11924  xrmaxiflemlub  11926  divalglemeuneg  12602  bezoutlemnewy  12685  4sqlemsdc  13091  ctiunctlemfo  13179  mhmmnd  13822  txmetcnp  15370  mulcncf  15460  suplociccreex  15476  cnplimclemr  15521  limccnpcntop  15527  lgsval  15864