Theorem ad5antlr 734

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  simp-5r  785  fimaproj  8121  restmetu  24079  foresf1o  31742  2ndresdju  31874  nn0xmulclb  31984  isdrng4  32395  elrspunidl  32546  elrspunsn  32547  rhmpreimaprmidl  32570  fedgmul  32716  locfinreflem  32820  pstmxmet  32877  satfdmlem  34359  mblfinlem3  36527  itg2gt0cn  36543  dffltz  41376  pell1234qrmulcl  41593  suplesup  44049  limclner  44367  bgoldbtbnd  46477  isomushgr  46494