Theorem ad5antlr 748

Description: Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad5antlr	⊢ ((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Proof of Theorem ad5antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 487	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad4antr 745	1 ⊢ ((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  simp-5r  798  fimaproj  8133  chnso  18712  isdrng4  20902  rhmpreimaprmidl  21542  restmetu  24796  foresf1o  32979  2ndresdju  33122  nn0xmulclb  33242  gsumwrd2dccatlem  33517  fracfld  33749  elrspunidl  33856  elrspunsn  33857  1arithidom  33947  mplvrpmga  34055  fedgmul  34141  locfinreflem  34350  pstmxmet  34407  satfdmlem  35947  mblfinlem3  38408  itg2gt0cn  38424  dffltz  43480  pell1234qrmulcl  43696  suplesup  46169  limclner  46479  bgoldbtbnd  48725  gricushgr  48833