Theorem ad4antlr 733

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 481	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad3antrrr 730	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-4r  783  ttrcltr  9669  initoeu2  17978  cpmatacl  22603  cpmatmcllem  22605  cpmatmcl  22606  chfacfisf  22741  chfacfisfcpmat  22742  restcld  23059  pthaus  23525  txhaus  23534  xkohaus  23540  alexsubALTlem4  23937  ustuqtop3  24131  ulmcau  26304  2sqreulem1  27357  2sqreunnlem1  27360  clwlkclwwlklem2  29929  gsumwun  33005  rhmimaidl  33403  qsidomlem1  33423  qsdrngi  33466  pidufd  33514  dimkerim  33623  fedgmul  33627  constrfiss  33741  locfinreflem  33830  cmpcref  33840  pstmxmet  33887  sigapildsys  34152  ldgenpisyslem1  34153  signstfvneq0  34563  nn0prpwlem  36310  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem29  37643  heicant  37649  mblfinlem3  37653  mblfinlem4  37654  itg2addnclem2  37666  itg2gt0cn  37669  ftc1cnnc  37686  sstotbnd2  37768  pell1234qrdich  42849  jm2.26lem3  42990  cvgdvgrat  44302  limsupgtlem  45775  limsupub2  45810  xlimmnfv  45832  icccncfext  45885  fourierdlem34  46139  fourierdlem87  46191  etransclem35  46267  smfaddlem1  46761  sfprmdvdsmersenne  47604  sbgoldbwt  47778  bgoldbtbnd  47810  isuspgrim0  47894  ply1mulgsumlem2  48376  nn0sumshdiglemA  48608