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  9747  initoeu2  18223  qsidomlem1  21669  matunitlindflem1  23027  matunitlindflem2  23028  cpmatacl  23067  cpmatmcllem  23069  cpmatmcl  23070  chfacfisf  23205  chfacfisfcpmat  23206  restcld  23523  pthaus  23990  txhaus  23999  xkohaus  24005  alexsubALTlem4  24402  ustuqtop3  24595  ulmcau  26755  2sqreulem1  27806  2sqreunnlem1  27809  clwlkclwwlklem2  30624  gsumwun  33713  rhmimaidl  34066  qsdrngi  34103  pidufd  34159  dimkerim  34342  fedgmul  34346  constrfiss  34466  locfinreflem  34555  cmpcref  34565  pstmxmet  34612  sigapildsys  34878  ldgenpisyslem1  34879  signstfvneq0  35284  nn0prpwlem  37301  poimirlem29  38772  heicant  38778  mblfinlem3  38782  mblfinlem4  38783  itg2addnclem2  38795  itg2gt0cn  38798  ftc1cnnc  38815  sstotbnd2  38911  pell1234qrdich  44072  jm2.26lem3  44212  cvgdvgrat  45500  limsupgtlem  47002  limsupub2  47037  xlimmnfv  47059  icccncfext  47112  fourierdlem34  47366  fourierdlem87  47418  etransclem35  47494  smfaddlem1  47988  sfprmdvdsmersenne  48903  sbgoldbwt  49090  bgoldbtbnd  49122  isuspgrim0  49207  ply1mulgsumlem2  49714  nn0sumshdiglemA  49946  itscnhlinecirc02p  50112