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 481	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad3antrrr 729	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  9785  initoeu2  18083  cpmatacl  22743  cpmatmcllem  22745  cpmatmcl  22746  chfacfisf  22881  chfacfisfcpmat  22882  restcld  23201  pthaus  23667  txhaus  23676  xkohaus  23682  alexsubALTlem4  24079  ustuqtop3  24273  ulmcau  26456  2sqreulem1  27508  2sqreunnlem1  27511  clwlkclwwlklem2  30032  rhmimaidl  33425  qsidomlem1  33445  qsdrngi  33488  pidufd  33536  dimkerim  33640  fedgmul  33644  locfinreflem  33786  cmpcref  33796  pstmxmet  33843  sigapildsys  34126  ldgenpisyslem1  34127  signstfvneq0  34549  nn0prpwlem  36288  matunitlindflem1  37576  matunitlindflem2  37577  poimirlem29  37609  heicant  37615  mblfinlem3  37619  mblfinlem4  37620  itg2addnclem2  37632  itg2gt0cn  37635  ftc1cnnc  37652  sstotbnd2  37734  pell1234qrdich  42817  jm2.26lem3  42958  cvgdvgrat  44282  limsupgtlem  45698  limsupub2  45733  xlimmnfv  45755  icccncfext  45808  fourierdlem34  46062  fourierdlem87  46114  etransclem35  46190  smfaddlem1  46684  sfprmdvdsmersenne  47477  sbgoldbwt  47651  bgoldbtbnd  47683  isuspgrim0  47756  ply1mulgsumlem2  48116  nn0sumshdiglemA  48353