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  7394  ctssdclemn0  7403  cauappcvgprlemladdfu  7974  caucvgprlemloc  7995  caucvgprlemladdfu  7997  caucvgprlemlim  8001  caucvgprprlemml  8014  caucvgprprlemloc  8023  caucvgprprlemlim  8031  suplocexprlemmu  8038  suplocexprlemru  8039  suplocexprlemloc  8041  suplocsrlem  8128  axcaucvglemres  8219  nn0ltexp2  11079  resqrexlemglsq  11715  xrmaxifle  11939  xrmaxiflemlub  11941  divalglemeuneg  12617  bezoutlemnewy  12700  4sqlemsdc  13106  ctiunctlemfo  13211  mhmmnd  13854  txmetcnp  15432  mulcncf  15522  suplociccreex  15538  cnplimclemr  15583  limccnpcntop  15589  lgsval  15926