Theorem ad4ant14 750

Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)

Hypothesis

Ref	Expression
ad4ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad4ant14	⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒)

Proof of Theorem ad4ant14

Step	Hyp	Ref	Expression
1		ad4ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantlr 713	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	adantlr 713	1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  ad5ant15  757  ad5ant25  760  soisoi  7324  dfac9  10130  lediv12a  12106  leexp1a  14139  seqcoll  14424  lo1bdd2  15467  rlimcld2  15521  rlimcn1  15531  isercolllem1  15610  summo  15662  climcnds  15796  geomulcvg  15821  mertenslem2  15830  prodmolem2  15878  prodmo  15879  fprod2d  15924  pwsle  17437  isacs2  17596  grprinvlem  18591  gsumpropd2lem  18597  gsumwsubmcl  18717  gsumwmhm  18725  mulgfval  18951  gaid  19162  gsmsymgrfixlem1  19294  mulgnn0di  19692  gsumval3  19774  fvmptnn04if  22350  cnpnei  22767  lfinun  23028  xkopt  23158  isr0  23240  fbflim  23479  alexsubALTlem3  23552  metss  24016  iscmet3lem2  24808  ovoliunlem3  25020  mbfposr  25168  i1fmulclem  25219  itg10a  25227  iblss  25321  dvlip  25509  plyeq0lem  25723  mtest  25915  itgulm  25919  dchrisumlem3  26991  rpvmasum2  27012  pntlem3  27109  nosupbday  27205  noinfbday  27220  hlpasch  28004  f1otrg  28119  lfgrwlkprop  28941  wlkiswwlks1  29118  frgrnbnb  29543  frgr2wwlkeqm  29581  unidifsnne  31768  hashxpe  32014  ccatf1  32110  signstfvneq0  33578  bnj605  33913  matunitlindflem1  36479  matunitlindflem2  36480  poimirlem26  36509  mblfinlem2  36521  ssfiunibd  44009  xralrple2  44054  infleinf  44072  infxrpnf  44146  fprodcn  44306  limsupub  44410  limsuppnflem  44416  limsupmnflem  44426  cnrefiisplem  44535  climxlim2lem  44551  icccncfext  44593  cncficcgt0  44594  cncfioobd  44603  dvbdfbdioolem2  44635  itgspltprt  44685  stoweidlem34  44740  stoweidlem49  44755  stoweidlem57  44763  fourierdlem34  44847  fourierdlem39  44852  fourierdlem50  44862  fourierdlem51  44863  fourierdlem64  44876  fourierdlem73  44885  fourierdlem77  44889  fourierdlem81  44893  fourierdlem94  44906  fourierdlem97  44909  fourierdlem103  44915  fourierdlem104  44916  fourierdlem113  44925  fourier2  44933  etransclem24  44964  intsal  45036  sge0pr  45100  sge0iunmptlemfi  45119  sge0seq  45152  sge0reuz  45153  nnfoctbdjlem  45161  meadjiunlem  45171  ismeannd  45173  carageniuncllem2  45228  isomennd  45237  hoicvr  45254  hspmbllem2  45333  iunhoiioolem  45381  iunhoiioo  45382  vonioo  45388  vonicc  45391  preimageiingt  45426  preimaleiinlt  45427  smfaddlem1  45469  smfaddlem2  45470  smflimlem4  45480  smfrec  45495  smfinflem  45523  sprsymrelf1lem  46149  lighneallem3  46265  isomgreqve  46483  subrngint  46729  1arymaptfo  47319