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  7303  dfac9  10090  lediv12a  12076  leexp1a  14140  seqcoll  14429  lo1bdd2  15490  rlimcld2  15544  rlimcn1  15554  isercolllem1  15631  summo  15683  climcnds  15817  geomulcvg  15842  mertenslem2  15851  prodmolem2  15901  prodmo  15902  fprod2d  15947  pwsle  17455  isacs2  17614  grpinvalem  18600  gsumpropd2lem  18606  gsumwsubmcl  18764  gsumwmhm  18772  mulgfval  19001  gaid  19231  gsmsymgrfixlem1  19357  mulgnn0di  19755  gsumval3  19837  subrngint  20469  fvmptnn04if  22736  cnpnei  23151  lfinun  23412  xkopt  23542  isr0  23624  fbflim  23863  alexsubALTlem3  23936  metss  24396  iscmet3lem2  25192  ovoliunlem3  25405  mbfposr  25553  i1fmulclem  25603  itg10a  25611  iblss  25706  dvlip  25898  plyeq0lem  26115  mtest  26313  itgulm  26317  dchrisumlem3  27402  rpvmasum2  27423  pntlem3  27520  nosupbday  27617  noinfbday  27632  hlpasch  28683  f1otrg  28798  lfgrwlkprop  29615  wlkiswwlks1  29797  frgrnbnb  30222  frgr2wwlkeqm  30260  unidifsnne  32465  hashxpe  32732  ccatf1  32870  fxpsubm  33129  cos9thpiminplylem1  33772  signstfvneq0  34563  bnj605  34897  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem26  37640  mblfinlem2  37652  ssfiunibd  45307  xralrple2  45350  infleinf  45368  infxrpnf  45442  fprodcn  45598  limsupub  45702  limsuppnflem  45708  limsupmnflem  45718  cnrefiisplem  45827  climxlim2lem  45843  icccncfext  45885  cncficcgt0  45886  cncfioobd  45895  dvbdfbdioolem2  45927  dvmptfprod  45943  itgspltprt  45977  stoweidlem34  46032  stoweidlem49  46047  stoweidlem57  46055  fourierdlem34  46139  fourierdlem39  46144  fourierdlem50  46154  fourierdlem51  46155  fourierdlem64  46168  fourierdlem73  46177  fourierdlem77  46181  fourierdlem81  46185  fourierdlem94  46198  fourierdlem97  46201  fourierdlem103  46207  fourierdlem104  46208  fourierdlem113  46217  fourier2  46225  etransclem24  46256  intsal  46328  sge0pr  46392  sge0iunmptlemfi  46411  sge0seq  46444  sge0reuz  46445  nnfoctbdjlem  46453  meadjiunlem  46463  ismeannd  46465  carageniuncllem2  46520  isomennd  46529  hoicvr  46546  hspmbllem2  46625  iunhoiioolem  46673  iunhoiioo  46674  vonioo  46680  vonicc  46683  preimageiingt  46718  preimaleiinlt  46719  smfaddlem1  46761  smfaddlem2  46762  smflimlem4  46772  smfrec  46787  smfinflem  46815  sprsymrelf1lem  47489  lighneallem3  47605  1arymaptfo  48629