Theorem ad4ant14 752

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 715	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	adantlr 715	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  758  ad5ant25  761  soisoi  7257  dfac9  10023  lediv12a  12010  leexp1a  14077  seqcoll  14366  lo1bdd2  15426  rlimcld2  15480  rlimcn1  15490  isercolllem1  15567  summo  15619  climcnds  15753  geomulcvg  15778  mertenslem2  15787  prodmolem2  15837  prodmo  15838  fprod2d  15883  pwsle  17391  isacs2  17554  grpinvalem  18576  gsumpropd2lem  18582  gsumwsubmcl  18740  gsumwmhm  18748  mulgfval  18977  gaid  19206  gsmsymgrfixlem1  19334  mulgnn0di  19732  gsumval3  19814  subrngint  20470  fvmptnn04if  22759  cnpnei  23174  lfinun  23435  xkopt  23565  isr0  23647  fbflim  23886  alexsubALTlem3  23959  metss  24418  iscmet3lem2  25214  ovoliunlem3  25427  mbfposr  25575  i1fmulclem  25625  itg10a  25633  iblss  25728  dvlip  25920  plyeq0lem  26137  mtest  26335  itgulm  26339  dchrisumlem3  27424  rpvmasum2  27445  pntlem3  27542  nosupbday  27639  noinfbday  27654  hlpasch  28729  f1otrg  28844  lfgrwlkprop  29659  wlkiswwlks1  29840  frgrnbnb  30265  frgr2wwlkeqm  30303  unidifsnne  32508  hashxpe  32781  ccatf1  32922  fxpsubm  33133  fxpsubrg  33135  mplvrpmmhm  33568  mplvrpmrhm  33569  cos9thpiminplylem1  33787  signstfvneq0  34577  bnj605  34911  matunitlindflem1  37656  matunitlindflem2  37657  poimirlem26  37686  mblfinlem2  37698  ssfiunibd  45350  xralrple2  45393  infleinf  45410  infxrpnf  45484  fprodcn  45640  limsupub  45742  limsuppnflem  45748  limsupmnflem  45758  cnrefiisplem  45867  climxlim2lem  45883  icccncfext  45925  cncficcgt0  45926  cncfioobd  45935  dvbdfbdioolem2  45967  dvmptfprod  45983  itgspltprt  46017  stoweidlem34  46072  stoweidlem49  46087  stoweidlem57  46095  fourierdlem34  46179  fourierdlem39  46184  fourierdlem50  46194  fourierdlem51  46195  fourierdlem64  46208  fourierdlem73  46217  fourierdlem77  46221  fourierdlem81  46225  fourierdlem94  46238  fourierdlem97  46241  fourierdlem103  46247  fourierdlem104  46248  fourierdlem113  46257  fourier2  46265  etransclem24  46296  intsal  46368  sge0pr  46432  sge0iunmptlemfi  46451  sge0seq  46484  sge0reuz  46485  nnfoctbdjlem  46493  meadjiunlem  46503  ismeannd  46505  carageniuncllem2  46560  isomennd  46569  hoicvr  46586  hspmbllem2  46665  iunhoiioolem  46713  iunhoiioo  46714  vonioo  46720  vonicc  46723  preimageiingt  46758  preimaleiinlt  46759  smfaddlem1  46801  smfaddlem2  46802  smflimlem4  46812  smfrec  46827  smfinflem  46855  sprsymrelf1lem  47522  lighneallem3  47638  1arymaptfo  48675