Theorem ad4antlr 729

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 726	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 206  df-an 396

This theorem is referenced by:  simp-4r  780  ttrcltr  9435  initoeu2  17712  cpmatacl  21846  cpmatmcllem  21848  cpmatmcl  21849  chfacfisf  21984  chfacfisfcpmat  21985  restcld  22304  pthaus  22770  txhaus  22779  xkohaus  22785  alexsubALTlem4  23182  ustuqtop3  23376  ulmcau  25535  2sqreulem1  26575  2sqreunnlem1  26578  clwlkclwwlklem2  28343  rhmimaidl  31588  qsidomlem1  31607  dimkerim  31687  fedgmul  31691  locfinreflem  31769  cmpcref  31779  pstmxmet  31826  sigapildsys  32109  ldgenpisyslem1  32110  signstfvneq0  32530  nn0prpwlem  34490  matunitlindflem1  35752  matunitlindflem2  35753  poimirlem29  35785  heicant  35791  mblfinlem3  35795  mblfinlem4  35796  itg2addnclem2  35808  itg2gt0cn  35811  ftc1cnnc  35828  sstotbnd2  35911  pell1234qrdich  40663  jm2.26lem3  40803  cvgdvgrat  41884  limsupgtlem  43272  limsupub2  43307  xlimmnfv  43329  icccncfext  43382  fourierdlem34  43636  fourierdlem87  43688  etransclem35  43764  smfaddlem1  44249  sfprmdvdsmersenne  45007  sbgoldbwt  45181  bgoldbtbnd  45213  ply1mulgsumlem2  45680  nn0sumshdiglemA  45917