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  784  ttrcltr  9756  initoeu2  18061  cpmatacl  22722  cpmatmcllem  22724  cpmatmcl  22725  chfacfisf  22860  chfacfisfcpmat  22861  restcld  23180  pthaus  23646  txhaus  23655  xkohaus  23661  alexsubALTlem4  24058  ustuqtop3  24252  ulmcau  26438  2sqreulem1  27490  2sqreunnlem1  27493  clwlkclwwlklem2  30019  gsumwun  33068  rhmimaidl  33460  qsidomlem1  33480  qsdrngi  33523  pidufd  33571  dimkerim  33678  fedgmul  33682  locfinreflem  33839  cmpcref  33849  pstmxmet  33896  sigapildsys  34163  ldgenpisyslem1  34164  signstfvneq0  34587  nn0prpwlem  36323  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem29  37656  heicant  37662  mblfinlem3  37666  mblfinlem4  37667  itg2addnclem2  37679  itg2gt0cn  37682  ftc1cnnc  37699  sstotbnd2  37781  pell1234qrdich  42872  jm2.26lem3  43013  cvgdvgrat  44332  limsupgtlem  45792  limsupub2  45827  xlimmnfv  45849  icccncfext  45902  fourierdlem34  46156  fourierdlem87  46208  etransclem35  46284  smfaddlem1  46778  sfprmdvdsmersenne  47590  sbgoldbwt  47764  bgoldbtbnd  47796  isuspgrim0  47872  ply1mulgsumlem2  48304  nn0sumshdiglemA  48540