Theorem ad4antlr 746

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  simp-4r  796  ttrcltr  9720  initoeu2  18196  qsidomlem1  21641  matunitlindflem1  22999  matunitlindflem2  23000  cpmatacl  23039  cpmatmcllem  23041  cpmatmcl  23042  chfacfisf  23177  chfacfisfcpmat  23178  restcld  23495  pthaus  23962  txhaus  23971  xkohaus  23977  alexsubALTlem4  24374  ustuqtop3  24567  ulmcau  26727  2sqreulem1  27778  2sqreunnlem1  27781  clwlkclwwlklem2  30596  gsumwun  33683  rhmimaidl  34028  qsdrngi  34065  pidufd  34121  dimkerim  34305  fedgmul  34309  constrfiss  34429  locfinreflem  34518  cmpcref  34528  pstmxmet  34575  sigapildsys  34841  ldgenpisyslem1  34842  signstfvneq0  35247  nn0prpwlem  37202  poimirlem29  38660  heicant  38666  mblfinlem3  38670  mblfinlem4  38671  itg2addnclem2  38683  itg2gt0cn  38686  ftc1cnnc  38703  sstotbnd2  38801  pell1234qrdich  43961  jm2.26lem3  44101  cvgdvgrat  45390  limsupgtlem  46880  limsupub2  46915  xlimmnfv  46937  icccncfext  46990  fourierdlem34  47244  fourierdlem87  47296  etransclem35  47372  smfaddlem1  47866  sfprmdvdsmersenne  48781  sbgoldbwt  48968  bgoldbtbnd  49000  isuspgrim0  49085  ply1mulgsumlem2  49592  nn0sumshdiglemA  49824  itscnhlinecirc02p  49990