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  7271  dfac9  10039  lediv12a  12026  leexp1a  14089  seqcoll  14378  lo1bdd2  15438  rlimcld2  15492  rlimcn1  15502  isercolllem1  15579  summo  15631  climcnds  15765  geomulcvg  15790  mertenslem2  15799  prodmolem2  15849  prodmo  15850  fprod2d  15895  pwsle  17404  isacs2  17567  grpinvalem  18589  gsumpropd2lem  18595  gsumwsubmcl  18753  gsumwmhm  18761  mulgfval  18990  gaid  19219  gsmsymgrfixlem1  19347  mulgnn0di  19745  gsumval3  19827  subrngint  20484  fvmptnn04if  22784  cnpnei  23199  lfinun  23460  xkopt  23590  isr0  23672  fbflim  23911  alexsubALTlem3  23984  metss  24443  iscmet3lem2  25239  ovoliunlem3  25452  mbfposr  25600  i1fmulclem  25650  itg10a  25658  iblss  25753  dvlip  25945  plyeq0lem  26162  mtest  26360  itgulm  26364  dchrisumlem3  27449  rpvmasum2  27470  pntlem3  27567  nosupbday  27664  noinfbday  27679  hlpasch  28754  f1otrg  28869  lfgrwlkprop  29685  wlkiswwlks1  29866  frgrnbnb  30294  frgr2wwlkeqm  30332  unidifsnne  32537  hashxpe  32815  ccatf1  32959  fxpsubm  33182  fxpsubrg  33184  mplvrpmmhm  33639  mplvrpmrhm  33640  vieta  33664  cos9thpiminplylem1  33867  signstfvneq0  34657  bnj605  34991  matunitlindflem1  37729  matunitlindflem2  37730  poimirlem26  37759  mblfinlem2  37771  ssfiunibd  45473  xralrple2  45515  infleinf  45532  infxrpnf  45606  fprodcn  45762  limsupub  45864  limsuppnflem  45870  limsupmnflem  45880  cnrefiisplem  45989  climxlim2lem  46005  icccncfext  46047  cncficcgt0  46048  cncfioobd  46057  dvbdfbdioolem2  46089  dvmptfprod  46105  itgspltprt  46139  stoweidlem34  46194  stoweidlem49  46209  stoweidlem57  46217  fourierdlem34  46301  fourierdlem39  46306  fourierdlem50  46316  fourierdlem51  46317  fourierdlem64  46330  fourierdlem73  46339  fourierdlem77  46343  fourierdlem81  46347  fourierdlem94  46360  fourierdlem97  46363  fourierdlem103  46369  fourierdlem104  46370  fourierdlem113  46379  fourier2  46387  etransclem24  46418  intsal  46490  sge0pr  46554  sge0iunmptlemfi  46573  sge0seq  46606  sge0reuz  46607  nnfoctbdjlem  46615  meadjiunlem  46625  ismeannd  46627  carageniuncllem2  46682  isomennd  46691  hoicvr  46708  hspmbllem2  46787  iunhoiioolem  46835  iunhoiioo  46836  vonioo  46842  vonicc  46845  preimageiingt  46880  preimaleiinlt  46881  smfaddlem1  46923  smfaddlem2  46924  smflimlem4  46934  smfrec  46949  smfinflem  46977  sprsymrelf1lem  47653  lighneallem3  47769  1arymaptfo  48805