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  9631  initoeu2  17941  cpmatacl  22619  cpmatmcllem  22621  cpmatmcl  22622  chfacfisf  22757  chfacfisfcpmat  22758  restcld  23075  pthaus  23541  txhaus  23550  xkohaus  23556  alexsubALTlem4  23953  ustuqtop3  24147  ulmcau  26320  2sqreulem1  27373  2sqreunnlem1  27376  clwlkclwwlklem2  29962  gsumwun  33031  rhmimaidl  33379  qsidomlem1  33399  qsdrngi  33442  pidufd  33490  dimkerim  33599  fedgmul  33603  constrfiss  33717  locfinreflem  33806  cmpcref  33816  pstmxmet  33863  sigapildsys  34128  ldgenpisyslem1  34129  signstfvneq0  34539  nn0prpwlem  36295  matunitlindflem1  37595  matunitlindflem2  37596  poimirlem29  37628  heicant  37634  mblfinlem3  37638  mblfinlem4  37639  itg2addnclem2  37651  itg2gt0cn  37654  ftc1cnnc  37671  sstotbnd2  37753  pell1234qrdich  42834  jm2.26lem3  42974  cvgdvgrat  44286  limsupgtlem  45759  limsupub2  45794  xlimmnfv  45816  icccncfext  45869  fourierdlem34  46123  fourierdlem87  46175  etransclem35  46251  smfaddlem1  46745  sfprmdvdsmersenne  47588  sbgoldbwt  47762  bgoldbtbnd  47794  isuspgrim0  47879  ply1mulgsumlem2  48373  nn0sumshdiglemA  48605