Theorem ad4antlr 732

Description: Deduction adding 4 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
ad4antlr	⊢ (((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem ad4antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 485	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad3antrrr 729	1 ⊢ (((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  simp-4r  783  initoeu2  17268  cpmatacl  21321  cpmatmcllem  21323  cpmatmcl  21324  chfacfisf  21459  chfacfisfcpmat  21460  restcld  21777  pthaus  22243  txhaus  22252  xkohaus  22258  alexsubALTlem4  22655  ustuqtop3  22849  ulmcau  24990  2sqreulem1  26030  2sqreunnlem1  26033  clwlkclwwlklem2  27785  rhmimaidl  31017  qsidomlem1  31036  dimkerim  31111  fedgmul  31115  locfinreflem  31193  cmpcref  31203  pstmxmet  31250  sigapildsys  31531  ldgenpisyslem1  31532  signstfvneq0  31952  nn0prpwlem  33783  matunitlindflem1  35053  matunitlindflem2  35054  poimirlem29  35086  heicant  35092  mblfinlem3  35096  mblfinlem4  35097  itg2addnclem2  35109  itg2gt0cn  35112  ftc1cnnc  35129  sstotbnd2  35212  pell1234qrdich  39802  jm2.26lem3  39942  cvgdvgrat  41017  limsupgtlem  42419  limsupub2  42454  xlimmnfv  42476  icccncfext  42529  fourierdlem34  42783  fourierdlem87  42835  etransclem35  42911  smfaddlem1  43396  sfprmdvdsmersenne  44121  sbgoldbwt  44295  bgoldbtbnd  44327  ply1mulgsumlem2  44795  nn0sumshdiglemA  45033