Theorem ad4antlr 746

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  simp-4r  796  ttrcltr  9695  initoeu2  18098  qsidomlem1  21517  cpmatacl  22910  cpmatmcllem  22912  cpmatmcl  22913  chfacfisf  23048  chfacfisfcpmat  23049  restcld  23366  pthaus  23832  txhaus  23841  xkohaus  23847  alexsubALTlem4  24244  ustuqtop3  24437  ulmcau  26595  2sqreulem1  27647  2sqreunnlem1  27650  clwlkclwwlklem2  30388  gsumwun  33427  rhmimaidl  33771  qsdrngi  33808  pidufd  33864  dimkerim  34048  fedgmul  34052  constrfiss  34172  locfinreflem  34261  cmpcref  34271  pstmxmet  34318  sigapildsys  34584  ldgenpisyslem1  34585  signstfvneq0  34991  nn0prpwlem  36874  matunitlindflem1  38308  matunitlindflem2  38309  poimirlem29  38341  heicant  38347  mblfinlem3  38351  mblfinlem4  38352  itg2addnclem2  38364  itg2gt0cn  38367  ftc1cnnc  38384  sstotbnd2  38466  pell1234qrdich  43629  jm2.26lem3  43769  cvgdvgrat  45064  limsupgtlem  46532  limsupub2  46567  xlimmnfv  46589  icccncfext  46642  fourierdlem34  46896  fourierdlem87  46948  etransclem35  47024  smfaddlem1  47518  sfprmdvdsmersenne  48396  sbgoldbwt  48583  bgoldbtbnd  48615  isuspgrim0  48700  ply1mulgsumlem2  49208  nn0sumshdiglemA  49440