Theorem ad4antlr 729

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  simp-4r  780  ttrcltr  9713  initoeu2  17970  cpmatacl  22438  cpmatmcllem  22440  cpmatmcl  22441  chfacfisf  22576  chfacfisfcpmat  22577  restcld  22896  pthaus  23362  txhaus  23371  xkohaus  23377  alexsubALTlem4  23774  ustuqtop3  23968  ulmcau  26143  2sqreulem1  27185  2sqreunnlem1  27188  clwlkclwwlklem2  29520  rhmimaidl  32824  qsidomlem1  32845  qsdrngi  32883  dimkerim  33000  fedgmul  33004  locfinreflem  33118  cmpcref  33128  pstmxmet  33175  sigapildsys  33458  ldgenpisyslem1  33459  signstfvneq0  33881  nn0prpwlem  35510  matunitlindflem1  36787  matunitlindflem2  36788  poimirlem29  36820  heicant  36826  mblfinlem3  36830  mblfinlem4  36831  itg2addnclem2  36843  itg2gt0cn  36846  ftc1cnnc  36863  sstotbnd2  36945  pell1234qrdich  41901  jm2.26lem3  42042  cvgdvgrat  43374  limsupgtlem  44791  limsupub2  44826  xlimmnfv  44848  icccncfext  44901  fourierdlem34  45155  fourierdlem87  45207  etransclem35  45283  smfaddlem1  45777  sfprmdvdsmersenne  46569  sbgoldbwt  46743  bgoldbtbnd  46775  ply1mulgsumlem2  47155  nn0sumshdiglemA  47392