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  8139  restmetu  24514  foresf1o  32490  2ndresdju  32632  nn0xmulclb  32753  chnso  32999  gsumwrd2dccatlem  33065  isdrng4  33294  fracfld  33307  elrspunidl  33448  elrspunsn  33449  rhmpreimaprmidl  33471  1arithidom  33557  fedgmul  33676  locfinreflem  33876  pstmxmet  33933  satfdmlem  35395  mblfinlem3  37688  itg2gt0cn  37704  dffltz  42632  pell1234qrmulcl  42853  suplesup  45346  limclner  45660  bgoldbtbnd  47803  gricushgr  47910