Theorem ad4antlr 734

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 731	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  9637  initoeu2  17983  cpmatacl  22681  cpmatmcllem  22683  cpmatmcl  22684  chfacfisf  22819  chfacfisfcpmat  22820  restcld  23137  pthaus  23603  txhaus  23612  xkohaus  23618  alexsubALTlem4  24015  ustuqtop3  24208  ulmcau  26360  2sqreulem1  27409  2sqreunnlem1  27412  clwlkclwwlklem2  30070  gsumwun  33137  rhmimaidl  33492  qsidomlem1  33512  qsdrngi  33555  pidufd  33603  dimkerim  33771  fedgmul  33775  constrfiss  33895  locfinreflem  33984  cmpcref  33994  pstmxmet  34041  sigapildsys  34306  ldgenpisyslem1  34307  signstfvneq0  34716  nn0prpwlem  36504  matunitlindflem1  37937  matunitlindflem2  37938  poimirlem29  37970  heicant  37976  mblfinlem3  37980  mblfinlem4  37981  itg2addnclem2  37993  itg2gt0cn  37996  ftc1cnnc  38013  sstotbnd2  38095  pell1234qrdich  43289  jm2.26lem3  43429  cvgdvgrat  44740  limsupgtlem  46205  limsupub2  46240  xlimmnfv  46262  icccncfext  46315  fourierdlem34  46569  fourierdlem87  46621  etransclem35  46697  smfaddlem1  47191  sfprmdvdsmersenne  48066  sbgoldbwt  48253  bgoldbtbnd  48285  isuspgrim0  48370  ply1mulgsumlem2  48863  nn0sumshdiglemA  49095