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  9606  initoeu2  17920  cpmatacl  22629  cpmatmcllem  22631  cpmatmcl  22632  chfacfisf  22767  chfacfisfcpmat  22768  restcld  23085  pthaus  23551  txhaus  23560  xkohaus  23566  alexsubALTlem4  23963  ustuqtop3  24156  ulmcau  26329  2sqreulem1  27382  2sqreunnlem1  27385  clwlkclwwlklem2  29975  gsumwun  33040  rhmimaidl  33392  qsidomlem1  33412  qsdrngi  33455  pidufd  33503  dimkerim  33635  fedgmul  33639  constrfiss  33759  locfinreflem  33848  cmpcref  33858  pstmxmet  33905  sigapildsys  34170  ldgenpisyslem1  34171  signstfvneq0  34580  nn0prpwlem  36355  matunitlindflem1  37655  matunitlindflem2  37656  poimirlem29  37688  heicant  37694  mblfinlem3  37698  mblfinlem4  37699  itg2addnclem2  37711  itg2gt0cn  37714  ftc1cnnc  37731  sstotbnd2  37813  pell1234qrdich  42893  jm2.26lem3  43033  cvgdvgrat  44345  limsupgtlem  45814  limsupub2  45849  xlimmnfv  45871  icccncfext  45924  fourierdlem34  46178  fourierdlem87  46230  etransclem35  46306  smfaddlem1  46800  sfprmdvdsmersenne  47633  sbgoldbwt  47807  bgoldbtbnd  47839  isuspgrim0  47924  ply1mulgsumlem2  48418  nn0sumshdiglemA  48650