Theorem ad5antlr 745

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 485	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad4antr 742	1 ⊢ ((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 400

This theorem is referenced by:  simp-5r  795  fimaproj  8110  chnso  18639  restmetu  24610  foresf1o  32652  2ndresdju  32801  nn0xmulclb  32923  gsumwrd2dccatlem  33218  isdrng4  33443  fracfld  33456  elrspunidl  33575  elrspunsn  33576  rhmpreimaprmidl  33599  1arithidom  33694  mplvrpmga  33803  fedgmul  33889  locfinreflem  34098  pstmxmet  34155  satfdmlem  35682  mblfinlem3  38122  itg2gt0cn  38138  dffltz  43180  pell1234qrmulcl  43396  suplesup  45879  limclner  46189  bgoldbtbnd  48395  gricushgr  48503