Theorem ad4antlr 734

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 731	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  9628  initoeu2  17974  cpmatacl  22691  cpmatmcllem  22693  cpmatmcl  22694  chfacfisf  22829  chfacfisfcpmat  22830  restcld  23147  pthaus  23613  txhaus  23622  xkohaus  23628  alexsubALTlem4  24025  ustuqtop3  24218  ulmcau  26373  2sqreulem1  27423  2sqreunnlem1  27426  clwlkclwwlklem2  30085  gsumwun  33152  rhmimaidl  33507  qsidomlem1  33527  qsdrngi  33570  pidufd  33618  dimkerim  33787  fedgmul  33791  constrfiss  33911  locfinreflem  34000  cmpcref  34010  pstmxmet  34057  sigapildsys  34322  ldgenpisyslem1  34323  signstfvneq0  34732  nn0prpwlem  36520  matunitlindflem1  37951  matunitlindflem2  37952  poimirlem29  37984  heicant  37990  mblfinlem3  37994  mblfinlem4  37995  itg2addnclem2  38007  itg2gt0cn  38010  ftc1cnnc  38027  sstotbnd2  38109  pell1234qrdich  43307  jm2.26lem3  43447  cvgdvgrat  44758  limsupgtlem  46223  limsupub2  46258  xlimmnfv  46280  icccncfext  46333  fourierdlem34  46587  fourierdlem87  46639  etransclem35  46715  smfaddlem1  47209  sfprmdvdsmersenne  48078  sbgoldbwt  48265  bgoldbtbnd  48297  isuspgrim0  48382  ply1mulgsumlem2  48875  nn0sumshdiglemA  49107