Theorem ad5antlr 735

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  simp-5r  786  fimaproj  8159  restmetu  24599  foresf1o  32532  2ndresdju  32666  nn0xmulclb  32782  chnso  32988  gsumwrd2dccatlem  33052  isdrng4  33279  fracfld  33290  elrspunidl  33436  elrspunsn  33437  rhmpreimaprmidl  33459  1arithidom  33545  fedgmul  33659  locfinreflem  33801  pstmxmet  33858  satfdmlem  35353  mblfinlem3  37646  itg2gt0cn  37662  dffltz  42621  pell1234qrmulcl  42843  suplesup  45289  limclner  45607  bgoldbtbnd  47734  gricushgr  47824