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  785  fimaproj  8114  restmetu  24458  foresf1o  32433  2ndresdju  32573  nn0xmulclb  32694  chnso  32940  gsumwrd2dccatlem  33006  isdrng4  33245  fracfld  33258  elrspunidl  33399  elrspunsn  33400  rhmpreimaprmidl  33422  1arithidom  33508  fedgmul  33627  locfinreflem  33830  pstmxmet  33887  satfdmlem  35355  mblfinlem3  37653  itg2gt0cn  37669  dffltz  42622  pell1234qrmulcl  42843  suplesup  45335  limclner  45649  bgoldbtbnd  47810  gricushgr  47917