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  7300  ctssdclemn0  7309  cauappcvgprlemladdfu  7874  caucvgprlemloc  7895  caucvgprlemladdfu  7897  caucvgprlemlim  7901  caucvgprprlemml  7914  caucvgprprlemloc  7923  caucvgprprlemlim  7931  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemloc  7941  suplocsrlem  8028  axcaucvglemres  8119  nn0ltexp2  10972  resqrexlemglsq  11584  xrmaxifle  11808  xrmaxiflemlub  11810  divalglemeuneg  12486  bezoutlemnewy  12569  4sqlemsdc  12975  ctiunctlemfo  13062  mhmmnd  13705  txmetcnp  15245  mulcncf  15335  suplociccreex  15351  cnplimclemr  15396  limccnpcntop  15402  lgsval  15736