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 481	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad4antr 731	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  8176  restmetu  24604  foresf1o  32532  2ndresdju  32667  nn0xmulclb  32778  chnso  32986  isdrng4  33264  fracfld  33275  elrspunidl  33421  elrspunsn  33422  rhmpreimaprmidl  33444  1arithidom  33530  fedgmul  33644  locfinreflem  33786  pstmxmet  33843  satfdmlem  35336  mblfinlem3  37619  itg2gt0cn  37635  dffltz  42589  pell1234qrmulcl  42811  suplesup  45254  limclner  45572  bgoldbtbnd  47683  gricushgr  47770