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  7294  ctssdclemn0  7303  cauappcvgprlemladdfu  7867  caucvgprlemloc  7888  caucvgprlemladdfu  7890  caucvgprlemlim  7894  caucvgprprlemml  7907  caucvgprprlemloc  7916  caucvgprprlemlim  7924  suplocexprlemmu  7931  suplocexprlemru  7932  suplocexprlemloc  7934  suplocsrlem  8021  axcaucvglemres  8112  nn0ltexp2  10964  resqrexlemglsq  11576  xrmaxifle  11800  xrmaxiflemlub  11802  divalglemeuneg  12477  bezoutlemnewy  12560  4sqlemsdc  12966  ctiunctlemfo  13053  mhmmnd  13696  txmetcnp  15235  mulcncf  15325  suplociccreex  15341  cnplimclemr  15386  limccnpcntop  15392  lgsval  15726