Theorem ad4antlr 732

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 729	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  783  ttrcltr  9739  initoeu2  18004  cpmatacl  22617  cpmatmcllem  22619  cpmatmcl  22620  chfacfisf  22755  chfacfisfcpmat  22756  restcld  23075  pthaus  23541  txhaus  23550  xkohaus  23556  alexsubALTlem4  23953  ustuqtop3  24147  ulmcau  26330  2sqreulem1  27378  2sqreunnlem1  27381  clwlkclwwlklem2  29809  rhmimaidl  33148  qsidomlem1  33168  qsdrngi  33206  dimkerim  33321  fedgmul  33325  locfinreflem  33441  cmpcref  33451  pstmxmet  33498  sigapildsys  33781  ldgenpisyslem1  33782  signstfvneq0  34204  nn0prpwlem  35806  matunitlindflem1  37089  matunitlindflem2  37090  poimirlem29  37122  heicant  37128  mblfinlem3  37132  mblfinlem4  37133  itg2addnclem2  37145  itg2gt0cn  37148  ftc1cnnc  37165  sstotbnd2  37247  pell1234qrdich  42281  jm2.26lem3  42422  cvgdvgrat  43750  limsupgtlem  45165  limsupub2  45200  xlimmnfv  45222  icccncfext  45275  fourierdlem34  45529  fourierdlem87  45581  etransclem35  45657  smfaddlem1  46151  sfprmdvdsmersenne  46943  sbgoldbwt  47117  bgoldbtbnd  47149  isuspgrim0  47170  ply1mulgsumlem2  47455  nn0sumshdiglemA  47692