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  9701  initoeu2  18171  qsidomlem1  21616  matunitlindflem1  22974  matunitlindflem2  22975  cpmatacl  23014  cpmatmcllem  23016  cpmatmcl  23017  chfacfisf  23152  chfacfisfcpmat  23153  restcld  23470  pthaus  23937  txhaus  23946  xkohaus  23952  alexsubALTlem4  24349  ustuqtop3  24542  ulmcau  26704  2sqreulem1  27755  2sqreunnlem1  27758  clwlkclwwlklem2  30573  gsumwun  33619  rhmimaidl  33964  qsdrngi  34001  pidufd  34057  dimkerim  34241  fedgmul  34245  constrfiss  34365  locfinreflem  34454  cmpcref  34464  pstmxmet  34511  sigapildsys  34777  ldgenpisyslem1  34778  signstfvneq0  35184  nn0prpwlem  37080  poimirlem29  38535  heicant  38541  mblfinlem3  38545  mblfinlem4  38546  itg2addnclem2  38558  itg2gt0cn  38561  ftc1cnnc  38578  sstotbnd2  38676  pell1234qrdich  43821  jm2.26lem3  43961  cvgdvgrat  45256  limsupgtlem  46731  limsupub2  46766  xlimmnfv  46788  icccncfext  46841  fourierdlem34  47095  fourierdlem87  47147  etransclem35  47223  smfaddlem1  47717  sfprmdvdsmersenne  48632  sbgoldbwt  48819  bgoldbtbnd  48851  isuspgrim0  48936  ply1mulgsumlem2  49443  nn0sumshdiglemA  49675