Theorem ad4antlr 733

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 730	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  9754  initoeu2  18070  cpmatacl  22738  cpmatmcllem  22740  cpmatmcl  22741  chfacfisf  22876  chfacfisfcpmat  22877  restcld  23196  pthaus  23662  txhaus  23671  xkohaus  23677  alexsubALTlem4  24074  ustuqtop3  24268  ulmcau  26453  2sqreulem1  27505  2sqreunnlem1  27508  clwlkclwwlklem2  30029  gsumwun  33051  rhmimaidl  33440  qsidomlem1  33460  qsdrngi  33503  pidufd  33551  dimkerim  33655  fedgmul  33659  locfinreflem  33801  cmpcref  33811  pstmxmet  33858  sigapildsys  34143  ldgenpisyslem1  34144  signstfvneq0  34566  nn0prpwlem  36305  matunitlindflem1  37603  matunitlindflem2  37604  poimirlem29  37636  heicant  37642  mblfinlem3  37646  mblfinlem4  37647  itg2addnclem2  37659  itg2gt0cn  37662  ftc1cnnc  37679  sstotbnd2  37761  pell1234qrdich  42849  jm2.26lem3  42990  cvgdvgrat  44309  limsupgtlem  45733  limsupub2  45768  xlimmnfv  45790  icccncfext  45843  fourierdlem34  46097  fourierdlem87  46149  etransclem35  46225  smfaddlem1  46719  sfprmdvdsmersenne  47528  sbgoldbwt  47702  bgoldbtbnd  47734  isuspgrim0  47810  ply1mulgsumlem2  48233  nn0sumshdiglemA  48469