Theorem ad5antlr 733

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  simp-5r  784  fimaproj  8138  restmetu  24509  foresf1o  32357  2ndresdju  32492  nn0xmulclb  32598  isdrng4  33044  fracfld  33055  elrspunidl  33206  elrspunsn  33207  rhmpreimaprmidl  33229  fedgmul  33399  locfinreflem  33511  pstmxmet  33568  satfdmlem  35048  mblfinlem3  37202  itg2gt0cn  37218  dffltz  42123  pell1234qrmulcl  42340  suplesup  44784  limclner  45102  bgoldbtbnd  47212  gricushgr  47295