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  7217  ctssdclemn0  7226  cauappcvgprlemladdfu  7782  caucvgprlemloc  7803  caucvgprlemladdfu  7805  caucvgprlemlim  7809  caucvgprprlemml  7822  caucvgprprlemloc  7831  caucvgprprlemlim  7839  suplocexprlemmu  7846  suplocexprlemru  7847  suplocexprlemloc  7849  suplocsrlem  7936  axcaucvglemres  8027  nn0ltexp2  10871  resqrexlemglsq  11403  xrmaxifle  11627  xrmaxiflemlub  11629  divalglemeuneg  12304  bezoutlemnewy  12387  4sqlemsdc  12793  ctiunctlemfo  12880  mhmmnd  13522  txmetcnp  15060  mulcncf  15150  suplociccreex  15166  cnplimclemr  15211  limccnpcntop  15217  lgsval  15551