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  7099  ctssdclemn0  7108  cauappcvgprlemladdfu  7652  caucvgprlemloc  7673  caucvgprlemladdfu  7675  caucvgprlemlim  7679  caucvgprprlemml  7692  caucvgprprlemloc  7701  caucvgprprlemlim  7709  suplocexprlemmu  7716  suplocexprlemru  7717  suplocexprlemloc  7719  suplocsrlem  7806  axcaucvglemres  7897  nn0ltexp2  10685  resqrexlemglsq  11026  xrmaxifle  11249  xrmaxiflemlub  11251  divalglemeuneg  11922  bezoutlemnewy  11991  ctiunctlemfo  12434  mhmmnd  12934  txmetcnp  13911  mulcncf  13984  suplociccreex  13995  cnplimclemr  14031  limccnpcntop  14037  lgsval  14298