Theorem ad4antlr 730

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 727	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  781  ttrcltr  9713  initoeu2  17978  cpmatacl  22573  cpmatmcllem  22575  cpmatmcl  22576  chfacfisf  22711  chfacfisfcpmat  22712  restcld  23031  pthaus  23497  txhaus  23506  xkohaus  23512  alexsubALTlem4  23909  ustuqtop3  24103  ulmcau  26286  2sqreulem1  27334  2sqreunnlem1  27337  clwlkclwwlklem2  29762  rhmimaidl  33056  qsidomlem1  33077  qsdrngi  33115  dimkerim  33230  fedgmul  33234  locfinreflem  33350  cmpcref  33360  pstmxmet  33407  sigapildsys  33690  ldgenpisyslem1  33691  signstfvneq0  34113  nn0prpwlem  35715  matunitlindflem1  36997  matunitlindflem2  36998  poimirlem29  37030  heicant  37036  mblfinlem3  37040  mblfinlem4  37041  itg2addnclem2  37053  itg2gt0cn  37056  ftc1cnnc  37073  sstotbnd2  37155  pell1234qrdich  42177  jm2.26lem3  42318  cvgdvgrat  43648  limsupgtlem  45065  limsupub2  45100  xlimmnfv  45122  icccncfext  45175  fourierdlem34  45429  fourierdlem87  45481  etransclem35  45557  smfaddlem1  46051  sfprmdvdsmersenne  46843  sbgoldbwt  47017  bgoldbtbnd  47049  ply1mulgsumlem2  47343  nn0sumshdiglemA  47580