Theorem ad4antlr 745

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 486	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad3antrrr 742	1 ⊢ (((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  simp-4r  795  ttrcltr  9686  initoeu2  18074  qsidomlem1  21461  cpmatacl  22854  cpmatmcllem  22856  cpmatmcl  22857  chfacfisf  22992  chfacfisfcpmat  22993  restcld  23310  pthaus  23776  txhaus  23785  xkohaus  23791  alexsubALTlem4  24188  ustuqtop3  24381  ulmcau  26539  2sqreulem1  27591  2sqreunnlem1  27594  clwlkclwwlklem2  30332  gsumwun  33377  rhmimaidl  33721  qsdrngi  33758  pidufd  33814  dimkerim  33998  fedgmul  34002  constrfiss  34122  locfinreflem  34211  cmpcref  34221  pstmxmet  34268  sigapildsys  34533  ldgenpisyslem1  34534  signstfvneq0  34940  nn0prpwlem  36814  matunitlindflem1  38248  matunitlindflem2  38249  poimirlem29  38281  heicant  38287  mblfinlem3  38291  mblfinlem4  38292  itg2addnclem2  38304  itg2gt0cn  38307  ftc1cnnc  38324  sstotbnd2  38406  pell1234qrdich  43571  jm2.26lem3  43711  cvgdvgrat  45006  limsupgtlem  46474  limsupub2  46509  xlimmnfv  46531  icccncfext  46584  fourierdlem34  46838  fourierdlem87  46890  etransclem35  46966  smfaddlem1  47460  sfprmdvdsmersenne  48338  sbgoldbwt  48525  bgoldbtbnd  48557  isuspgrim0  48642  ply1mulgsumlem2  49150  nn0sumshdiglemA  49382