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  7210  ctssdclemn0  7219  cauappcvgprlemladdfu  7774  caucvgprlemloc  7795  caucvgprlemladdfu  7797  caucvgprlemlim  7801  caucvgprprlemml  7814  caucvgprprlemloc  7823  caucvgprprlemlim  7831  suplocexprlemmu  7838  suplocexprlemru  7839  suplocexprlemloc  7841  suplocsrlem  7928  axcaucvglemres  8019  nn0ltexp2  10861  resqrexlemglsq  11377  xrmaxifle  11601  xrmaxiflemlub  11603  divalglemeuneg  12278  bezoutlemnewy  12361  4sqlemsdc  12767  ctiunctlemfo  12854  mhmmnd  13496  txmetcnp  15034  mulcncf  15124  suplociccreex  15140  cnplimclemr  15185  limccnpcntop  15191  lgsval  15525