Theorem ad4antlr 731

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 480	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad3antrrr 728	1 ⊢ (((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  simp-4r  782  ttrcltr  9749  initoeu2  18014  cpmatacl  22646  cpmatmcllem  22648  cpmatmcl  22649  chfacfisf  22784  chfacfisfcpmat  22785  restcld  23104  pthaus  23570  txhaus  23579  xkohaus  23585  alexsubALTlem4  23982  ustuqtop3  24176  ulmcau  26359  2sqreulem1  27407  2sqreunnlem1  27410  clwlkclwwlklem2  29838  rhmimaidl  33181  qsidomlem1  33201  qsdrngi  33239  dimkerim  33366  fedgmul  33370  locfinreflem  33482  cmpcref  33492  pstmxmet  33539  sigapildsys  33822  ldgenpisyslem1  33823  signstfvneq0  34245  nn0prpwlem  35847  matunitlindflem1  37130  matunitlindflem2  37131  poimirlem29  37163  heicant  37169  mblfinlem3  37173  mblfinlem4  37174  itg2addnclem2  37186  itg2gt0cn  37189  ftc1cnnc  37206  sstotbnd2  37288  pell1234qrdich  42330  jm2.26lem3  42471  cvgdvgrat  43799  limsupgtlem  45212  limsupub2  45247  xlimmnfv  45269  icccncfext  45322  fourierdlem34  45576  fourierdlem87  45628  etransclem35  45704  smfaddlem1  46198  sfprmdvdsmersenne  46990  sbgoldbwt  47164  bgoldbtbnd  47196  isuspgrim0  47266  ply1mulgsumlem2  47551  nn0sumshdiglemA  47788