Theorem ad5antlr 747

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  simp-5r  797  fimaproj  8119  chnso  18670  rhmpreimaprmidl  21439  restmetu  24688  foresf1o  32760  2ndresdju  32906  nn0xmulclb  33028  gsumwrd2dccatlem  33310  isdrng4  33531  fracfld  33544  elrspunidl  33652  elrspunsn  33653  1arithidom  33744  mplvrpmga  33852  fedgmul  33938  locfinreflem  34147  pstmxmet  34204  satfdmlem  35731  mblfinlem3  38170  itg2gt0cn  38186  dffltz  43228  pell1234qrmulcl  43444  suplesup  45913  limclner  46223  bgoldbtbnd  48429  gricushgr  48537