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  7167  ctssdclemn0  7176  cauappcvgprlemladdfu  7721  caucvgprlemloc  7742  caucvgprlemladdfu  7744  caucvgprlemlim  7748  caucvgprprlemml  7761  caucvgprprlemloc  7770  caucvgprprlemlim  7778  suplocexprlemmu  7785  suplocexprlemru  7786  suplocexprlemloc  7788  suplocsrlem  7875  axcaucvglemres  7966  nn0ltexp2  10801  resqrexlemglsq  11187  xrmaxifle  11411  xrmaxiflemlub  11413  divalglemeuneg  12088  bezoutlemnewy  12163  4sqlemsdc  12569  ctiunctlemfo  12656  mhmmnd  13246  txmetcnp  14754  mulcncf  14844  suplociccreex  14860  cnplimclemr  14905  limccnpcntop  14911  lgsval  15245