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  7284  dfac9  10059  lediv12a  12047  leexp1a  14110  seqcoll  14399  lo1bdd2  15459  rlimcld2  15513  rlimcn1  15523  isercolllem1  15600  summo  15652  climcnds  15786  geomulcvg  15811  mertenslem2  15820  prodmolem2  15870  prodmo  15871  fprod2d  15916  pwsle  17425  isacs2  17588  grpinvalem  18610  gsumpropd2lem  18616  gsumwsubmcl  18774  gsumwmhm  18782  mulgfval  19011  gaid  19240  gsmsymgrfixlem1  19368  mulgnn0di  19766  gsumval3  19848  subrngint  20505  fvmptnn04if  22805  cnpnei  23220  lfinun  23481  xkopt  23611  isr0  23693  fbflim  23932  alexsubALTlem3  24005  metss  24464  iscmet3lem2  25260  ovoliunlem3  25473  mbfposr  25621  i1fmulclem  25671  itg10a  25679  iblss  25774  dvlip  25966  plyeq0lem  26183  mtest  26381  itgulm  26385  dchrisumlem3  27470  rpvmasum2  27491  pntlem3  27588  nosupbday  27685  noinfbday  27700  addonbday  28287  hlpasch  28840  f1otrg  28955  lfgrwlkprop  29771  wlkiswwlks1  29952  frgrnbnb  30380  frgr2wwlkeqm  30418  unidifsnne  32623  hashxpe  32898  ccatf1  33042  fxpsubm  33266  fxpsubrg  33268  mplvrpmmhm  33723  mplvrpmrhm  33724  esplyfval1  33750  vieta  33757  cos9thpiminplylem1  33960  signstfvneq0  34750  bnj605  35083  matunitlindflem1  37867  matunitlindflem2  37868  poimirlem26  37897  mblfinlem2  37909  ssfiunibd  45671  xralrple2  45713  infleinf  45730  infxrpnf  45804  fprodcn  45960  limsupub  46062  limsuppnflem  46068  limsupmnflem  46078  cnrefiisplem  46187  climxlim2lem  46203  icccncfext  46245  cncficcgt0  46246  cncfioobd  46255  dvbdfbdioolem2  46287  dvmptfprod  46303  itgspltprt  46337  stoweidlem34  46392  stoweidlem49  46407  stoweidlem57  46415  fourierdlem34  46499  fourierdlem39  46504  fourierdlem50  46514  fourierdlem51  46515  fourierdlem64  46528  fourierdlem73  46537  fourierdlem77  46541  fourierdlem81  46545  fourierdlem94  46558  fourierdlem97  46561  fourierdlem103  46567  fourierdlem104  46568  fourierdlem113  46577  fourier2  46585  etransclem24  46616  intsal  46688  sge0pr  46752  sge0iunmptlemfi  46771  sge0seq  46804  sge0reuz  46805  nnfoctbdjlem  46813  meadjiunlem  46823  ismeannd  46825  carageniuncllem2  46880  isomennd  46889  hoicvr  46906  hspmbllem2  46985  iunhoiioolem  47033  iunhoiioo  47034  vonioo  47040  vonicc  47043  preimageiingt  47078  preimaleiinlt  47079  smfaddlem1  47121  smfaddlem2  47122  smflimlem4  47132  smfrec  47147  smfinflem  47175  sprsymrelf1lem  47851  lighneallem3  47967  1arymaptfo  49003