Theorem ad4ant14 753

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 716	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	adantlr 716	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:  ad5ant15  759  ad5ant25  762  soisoi  7276  dfac9  10050  lediv12a  12040  leexp1a  14128  seqcoll  14417  lo1bdd2  15477  rlimcld2  15531  rlimcn1  15541  isercolllem1  15618  summo  15670  climcnds  15807  geomulcvg  15832  mertenslem2  15841  prodmolem2  15891  prodmo  15892  fprod2d  15937  pwsle  17447  isacs2  17610  grpinvalem  18632  gsumpropd2lem  18638  gsumwsubmcl  18796  gsumwmhm  18804  mulgfval  19036  gaid  19265  gsmsymgrfixlem1  19393  mulgnn0di  19791  gsumval3  19873  subrngint  20528  fvmptnn04if  22824  cnpnei  23239  lfinun  23500  xkopt  23630  isr0  23712  fbflim  23951  alexsubALTlem3  24024  metss  24483  iscmet3lem2  25269  ovoliunlem3  25481  mbfposr  25629  i1fmulclem  25679  itg10a  25687  iblss  25782  dvlip  25970  plyeq0lem  26185  mtest  26382  itgulm  26386  dchrisumlem3  27468  rpvmasum2  27489  pntlem3  27586  nosupbday  27683  noinfbday  27698  addonbday  28285  hlpasch  28838  f1otrg  28953  lfgrwlkprop  29769  wlkiswwlks1  29950  frgrnbnb  30378  frgr2wwlkeqm  30416  unidifsnne  32621  hashxpe  32895  ccatf1  33024  fxpsubm  33248  fxpsubrg  33250  mplvrpmmhm  33705  mplvrpmrhm  33706  esplyfval1  33732  vieta  33739  cos9thpiminplylem1  33942  signstfvneq0  34732  bnj605  35065  matunitlindflem1  37951  matunitlindflem2  37952  poimirlem26  37981  mblfinlem2  37993  ssfiunibd  45760  xralrple2  45802  infleinf  45819  infxrpnf  45892  fprodcn  46048  limsupub  46150  limsuppnflem  46156  limsupmnflem  46166  cnrefiisplem  46275  climxlim2lem  46291  icccncfext  46333  cncficcgt0  46334  cncfioobd  46343  dvbdfbdioolem2  46375  dvmptfprod  46391  itgspltprt  46425  stoweidlem34  46480  stoweidlem49  46495  stoweidlem57  46503  fourierdlem34  46587  fourierdlem39  46592  fourierdlem50  46602  fourierdlem51  46603  fourierdlem64  46616  fourierdlem73  46625  fourierdlem77  46629  fourierdlem81  46633  fourierdlem94  46646  fourierdlem97  46649  fourierdlem103  46655  fourierdlem104  46656  fourierdlem113  46665  fourier2  46673  etransclem24  46704  intsal  46776  sge0pr  46840  sge0iunmptlemfi  46859  sge0seq  46892  sge0reuz  46893  nnfoctbdjlem  46901  meadjiunlem  46911  ismeannd  46913  carageniuncllem2  46968  isomennd  46977  hoicvr  46994  hspmbllem2  47073  iunhoiioolem  47121  iunhoiioo  47122  vonioo  47128  vonicc  47131  preimageiingt  47166  preimaleiinlt  47167  smfaddlem1  47209  smfaddlem2  47210  smflimlem4  47220  smfrec  47235  smfinflem  47263  sprsymrelf1lem  47963  lighneallem3  48082  1arymaptfo  49131