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  9699  initoeu2  18111  qsidomlem1  21549  matunitlindflem1  22907  matunitlindflem2  22908  cpmatacl  22947  cpmatmcllem  22949  cpmatmcl  22950  chfacfisf  23085  chfacfisfcpmat  23086  restcld  23403  pthaus  23870  txhaus  23879  xkohaus  23885  alexsubALTlem4  24282  ustuqtop3  24475  ulmcau  26638  2sqreulem1  27690  2sqreunnlem1  27693  clwlkclwwlklem2  30478  gsumwun  33524  rhmimaidl  33868  qsdrngi  33905  pidufd  33961  dimkerim  34145  fedgmul  34149  constrfiss  34269  locfinreflem  34358  cmpcref  34368  pstmxmet  34415  sigapildsys  34681  ldgenpisyslem1  34682  signstfvneq0  35088  nn0prpwlem  36949  poimirlem29  38406  heicant  38412  mblfinlem3  38416  mblfinlem4  38417  itg2addnclem2  38429  itg2gt0cn  38432  ftc1cnnc  38449  sstotbnd2  38532  pell1234qrdich  43710  jm2.26lem3  43850  cvgdvgrat  45145  limsupgtlem  46613  limsupub2  46648  xlimmnfv  46670  icccncfext  46723  fourierdlem34  46977  fourierdlem87  47029  etransclem35  47105  smfaddlem1  47599  sfprmdvdsmersenne  48514  sbgoldbwt  48701  bgoldbtbnd  48733  isuspgrim0  48818  ply1mulgsumlem2  49325  nn0sumshdiglemA  49557