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 398

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 399

This theorem is referenced by:  ad5ant15  757  ad5ant25  760  soisoi  7081  dfac9  9562  lediv12a  11533  leexp1a  13540  seqcoll  13823  lo1bdd2  14881  rlimcld2  14935  rlimcn1  14945  isercolllem1  15021  summo  15074  climcnds  15206  geomulcvg  15232  mertenslem2  15241  prodmolem2  15289  prodmo  15290  fprod2d  15335  pwsle  16765  isacs2  16924  grprinvlem  17883  gsumpropd2lem  17889  gsumwsubmcl  18001  gsumwmhm  18010  mulgfval  18226  gaid  18429  gsmsymgrfixlem1  18555  mulgnn0di  18946  gsumval3  19027  fvmptnn04if  21457  cnpnei  21872  lfinun  22133  xkopt  22263  isr0  22345  fbflim  22584  alexsubALTlem3  22657  metss  23118  iscmet3lem2  23895  ovoliunlem3  24105  mbfposr  24253  i1fmulclem  24303  itg10a  24311  iblss  24405  dvlip  24590  plyeq0lem  24800  mtest  24992  itgulm  24996  dchrisumlem3  26067  rpvmasum2  26088  pntlem3  26185  hlpasch  26542  f1otrg  26657  lfgrwlkprop  27469  wlkiswwlks1  27645  frgrnbnb  28072  frgr2wwlkeqm  28110  unidifsnne  30296  hashxpe  30529  ccatf1  30625  signstfvneq0  31842  bnj605  32179  matunitlindflem1  34903  matunitlindflem2  34904  poimirlem26  34933  mblfinlem2  34945  ssfiunibd  41625  xralrple2  41671  infleinf  41689  infxrpnf  41770  fprodcn  41930  limsupub  42034  limsuppnflem  42040  limsupmnflem  42050  cnrefiisplem  42159  climxlim2lem  42175  icccncfext  42219  cncficcgt0  42220  cncfioobd  42229  dvbdfbdioolem2  42263  itgspltprt  42313  stoweidlem34  42368  stoweidlem49  42383  stoweidlem57  42391  fourierdlem34  42475  fourierdlem39  42480  fourierdlem50  42490  fourierdlem51  42491  fourierdlem64  42504  fourierdlem73  42513  fourierdlem77  42517  fourierdlem81  42521  fourierdlem94  42534  fourierdlem97  42537  fourierdlem103  42543  fourierdlem104  42544  fourierdlem113  42553  fourier2  42561  etransclem24  42592  intsal  42662  sge0pr  42725  sge0iunmptlemfi  42744  sge0seq  42777  sge0reuz  42778  nnfoctbdjlem  42786  meadjiunlem  42796  ismeannd  42798  carageniuncllem2  42853  isomennd  42862  hoicvr  42879  hspmbllem2  42958  iunhoiioolem  43006  iunhoiioo  43007  vonioo  43013  vonicc  43016  preimageiingt  43047  preimaleiinlt  43048  smfaddlem1  43088  smfaddlem2  43089  smflimlem4  43099  smfrec  43113  smfinflem  43140  sprsymrelf1lem  43702  lighneallem3  43821  isomgreqve  44039