Theorem ad4antlr 743

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  simp-4r  793  ttrcltr  9668  initoeu2  18032  cpmatacl  22756  cpmatmcllem  22758  cpmatmcl  22759  chfacfisf  22894  chfacfisfcpmat  22895  restcld  23212  pthaus  23678  txhaus  23687  xkohaus  23693  alexsubALTlem4  24090  ustuqtop3  24283  ulmcau  26435  2sqreulem1  27487  2sqreunnlem1  27490  clwlkclwwlklem2  30148  gsumwun  33217  rhmimaidl  33579  qsidomlem1  33600  qsdrngi  33644  pidufd  33700  dimkerim  33885  fedgmul  33889  constrfiss  34009  locfinreflem  34098  cmpcref  34108  pstmxmet  34155  sigapildsys  34420  ldgenpisyslem1  34421  signstfvneq0  34830  nn0prpwlem  36646  matunitlindflem1  38079  matunitlindflem2  38080  poimirlem29  38112  heicant  38118  mblfinlem3  38122  mblfinlem4  38123  itg2addnclem2  38135  itg2gt0cn  38138  ftc1cnnc  38155  sstotbnd2  38237  pell1234qrdich  43402  jm2.26lem3  43542  cvgdvgrat  44853  limsupgtlem  46315  limsupub2  46350  xlimmnfv  46372  icccncfext  46425  fourierdlem34  46679  fourierdlem87  46731  etransclem35  46807  smfaddlem1  47301  sfprmdvdsmersenne  48176  sbgoldbwt  48363  bgoldbtbnd  48395  isuspgrim0  48480  ply1mulgsumlem2  48973  nn0sumshdiglemA  49205