Theorem ad4antlr 731

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  simp-4r  782  ttrcltr  9707  initoeu2  17962  cpmatacl  22209  cpmatmcllem  22211  cpmatmcl  22212  chfacfisf  22347  chfacfisfcpmat  22348  restcld  22667  pthaus  23133  txhaus  23142  xkohaus  23148  alexsubALTlem4  23545  ustuqtop3  23739  ulmcau  25898  2sqreulem1  26938  2sqreunnlem1  26941  clwlkclwwlklem2  29242  rhmimaidl  32538  qsidomlem1  32559  qsdrngi  32597  dimkerim  32700  fedgmul  32704  locfinreflem  32808  cmpcref  32818  pstmxmet  32865  sigapildsys  33148  ldgenpisyslem1  33149  signstfvneq0  33571  nn0prpwlem  35195  matunitlindflem1  36472  matunitlindflem2  36473  poimirlem29  36505  heicant  36511  mblfinlem3  36515  mblfinlem4  36516  itg2addnclem2  36528  itg2gt0cn  36531  ftc1cnnc  36548  sstotbnd2  36630  pell1234qrdich  41584  jm2.26lem3  41725  cvgdvgrat  43057  limsupgtlem  44479  limsupub2  44514  xlimmnfv  44536  icccncfext  44589  fourierdlem34  44843  fourierdlem87  44895  etransclem35  44971  smfaddlem1  45465  sfprmdvdsmersenne  46257  sbgoldbwt  46431  bgoldbtbnd  46463  ply1mulgsumlem2  47021  nn0sumshdiglemA  47258