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  9625  initoeu2  17940  cpmatacl  22660  cpmatmcllem  22662  cpmatmcl  22663  chfacfisf  22798  chfacfisfcpmat  22799  restcld  23116  pthaus  23582  txhaus  23591  xkohaus  23597  alexsubALTlem4  23994  ustuqtop3  24187  ulmcau  26360  2sqreulem1  27413  2sqreunnlem1  27416  clwlkclwwlklem2  30075  gsumwun  33158  rhmimaidl  33513  qsidomlem1  33533  qsdrngi  33576  pidufd  33624  dimkerim  33784  fedgmul  33788  constrfiss  33908  locfinreflem  33997  cmpcref  34007  pstmxmet  34054  sigapildsys  34319  ldgenpisyslem1  34320  signstfvneq0  34729  nn0prpwlem  36516  matunitlindflem1  37813  matunitlindflem2  37814  poimirlem29  37846  heicant  37852  mblfinlem3  37856  mblfinlem4  37857  itg2addnclem2  37869  itg2gt0cn  37872  ftc1cnnc  37889  sstotbnd2  37971  pell1234qrdich  43099  jm2.26lem3  43239  cvgdvgrat  44550  limsupgtlem  46017  limsupub2  46052  xlimmnfv  46074  icccncfext  46127  fourierdlem34  46381  fourierdlem87  46433  etransclem35  46509  smfaddlem1  47003  sfprmdvdsmersenne  47845  sbgoldbwt  48019  bgoldbtbnd  48051  isuspgrim0  48136  ply1mulgsumlem2  48629  nn0sumshdiglemA  48861