Theorem ad5antr 488

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 486	. 2 ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
3	2	adantr 274	1 ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad6antr  490  difinfinf  7035  ctssdclemn0  7044  cauappcvgprlemladdfu  7557  caucvgprlemloc  7578  caucvgprlemladdfu  7580  caucvgprlemlim  7584  caucvgprprlemml  7597  caucvgprprlemloc  7606  caucvgprprlemlim  7614  suplocexprlemmu  7621  suplocexprlemru  7622  suplocexprlemloc  7624  suplocsrlem  7711  axcaucvglemres  7802  resqrexlemglsq  10904  xrmaxifle  11125  xrmaxiflemlub  11127  divalglemeuneg  11795  bezoutlemnewy  11860  ctiunctlemfo  12140  txmetcnp  12878  mulcncf  12951  suplociccreex  12962  cnplimclemr  12998  limccnpcntop  13004