Theorem ad4antlr 734

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 731	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  784  ttrcltr  9637  initoeu2  17952  cpmatacl  22672  cpmatmcllem  22674  cpmatmcl  22675  chfacfisf  22810  chfacfisfcpmat  22811  restcld  23128  pthaus  23594  txhaus  23603  xkohaus  23609  alexsubALTlem4  24006  ustuqtop3  24199  ulmcau  26372  2sqreulem1  27425  2sqreunnlem1  27428  clwlkclwwlklem2  30087  gsumwun  33169  rhmimaidl  33524  qsidomlem1  33544  qsdrngi  33587  pidufd  33635  dimkerim  33804  fedgmul  33808  constrfiss  33928  locfinreflem  34017  cmpcref  34027  pstmxmet  34074  sigapildsys  34339  ldgenpisyslem1  34340  signstfvneq0  34749  nn0prpwlem  36535  matunitlindflem1  37861  matunitlindflem2  37862  poimirlem29  37894  heicant  37900  mblfinlem3  37904  mblfinlem4  37905  itg2addnclem2  37917  itg2gt0cn  37920  ftc1cnnc  37937  sstotbnd2  38019  pell1234qrdich  43212  jm2.26lem3  43352  cvgdvgrat  44663  limsupgtlem  46129  limsupub2  46164  xlimmnfv  46186  icccncfext  46239  fourierdlem34  46493  fourierdlem87  46545  etransclem35  46621  smfaddlem1  47115  sfprmdvdsmersenne  47957  sbgoldbwt  48131  bgoldbtbnd  48163  isuspgrim0  48248  ply1mulgsumlem2  48741  nn0sumshdiglemA  48973