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  8132  chnso  18681  isdrng4  20826  rhmpreimaprmidl  21460  restmetu  24708  foresf1o  32828  2ndresdju  32972  nn0xmulclb  33094  gsumwrd2dccatlem  33375  fracfld  33607  elrspunidl  33714  elrspunsn  33715  1arithidom  33805  mplvrpmga  33913  fedgmul  33999  locfinreflem  34208  pstmxmet  34265  satfdmlem  35838  mblfinlem3  38288  itg2gt0cn  38304  dffltz  43346  pell1234qrmulcl  43562  suplesup  46035  limclner  46345  bgoldbtbnd  48551  gricushgr  48659