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  7096  ctssdclemn0  7105  cauappcvgprlemladdfu  7649  caucvgprlemloc  7670  caucvgprlemladdfu  7672  caucvgprlemlim  7676  caucvgprprlemml  7689  caucvgprprlemloc  7698  caucvgprprlemlim  7706  suplocexprlemmu  7713  suplocexprlemru  7714  suplocexprlemloc  7716  suplocsrlem  7803  axcaucvglemres  7894  nn0ltexp2  10682  resqrexlemglsq  11023  xrmaxifle  11246  xrmaxiflemlub  11248  divalglemeuneg  11919  bezoutlemnewy  11988  ctiunctlemfo  12431  mhmmnd  12911  txmetcnp  13880  mulcncf  13953  suplociccreex  13964  cnplimclemr  14000  limccnpcntop  14006  lgsval  14267