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  7326  dfac9  10156  lediv12a  12140  leexp1a  14198  seqcoll  14487  lo1bdd2  15545  rlimcld2  15599  rlimcn1  15609  isercolllem1  15686  summo  15738  climcnds  15872  geomulcvg  15897  mertenslem2  15906  prodmolem2  15956  prodmo  15957  fprod2d  16002  pwsle  17511  isacs2  17670  grpinvalem  18656  gsumpropd2lem  18662  gsumwsubmcl  18820  gsumwmhm  18828  mulgfval  19057  gaid  19287  gsmsymgrfixlem1  19413  mulgnn0di  19811  gsumval3  19893  subrngint  20525  fvmptnn04if  22792  cnpnei  23207  lfinun  23468  xkopt  23598  isr0  23680  fbflim  23919  alexsubALTlem3  23992  metss  24452  iscmet3lem2  25249  ovoliunlem3  25462  mbfposr  25610  i1fmulclem  25660  itg10a  25668  iblss  25763  dvlip  25955  plyeq0lem  26172  mtest  26370  itgulm  26374  dchrisumlem3  27459  rpvmasum2  27480  pntlem3  27577  nosupbday  27674  noinfbday  27689  hlpasch  28740  f1otrg  28855  lfgrwlkprop  29672  wlkiswwlks1  29854  frgrnbnb  30279  frgr2wwlkeqm  30317  unidifsnne  32522  hashxpe  32791  ccatf1  32929  cos9thpiminplylem1  33821  signstfvneq0  34609  bnj605  34943  matunitlindflem1  37645  matunitlindflem2  37646  poimirlem26  37675  mblfinlem2  37687  ssfiunibd  45305  xralrple2  45348  infleinf  45366  infxrpnf  45440  fprodcn  45596  limsupub  45700  limsuppnflem  45706  limsupmnflem  45716  cnrefiisplem  45825  climxlim2lem  45841  icccncfext  45883  cncficcgt0  45884  cncfioobd  45893  dvbdfbdioolem2  45925  dvmptfprod  45941  itgspltprt  45975  stoweidlem34  46030  stoweidlem49  46045  stoweidlem57  46053  fourierdlem34  46137  fourierdlem39  46142  fourierdlem50  46152  fourierdlem51  46153  fourierdlem64  46166  fourierdlem73  46175  fourierdlem77  46179  fourierdlem81  46183  fourierdlem94  46196  fourierdlem97  46199  fourierdlem103  46205  fourierdlem104  46206  fourierdlem113  46215  fourier2  46223  etransclem24  46254  intsal  46326  sge0pr  46390  sge0iunmptlemfi  46409  sge0seq  46442  sge0reuz  46443  nnfoctbdjlem  46451  meadjiunlem  46461  ismeannd  46463  carageniuncllem2  46518  isomennd  46527  hoicvr  46544  hspmbllem2  46623  iunhoiioolem  46671  iunhoiioo  46672  vonioo  46678  vonicc  46681  preimageiingt  46716  preimaleiinlt  46717  smfaddlem1  46759  smfaddlem2  46760  smflimlem4  46770  smfrec  46785  smfinflem  46813  sprsymrelf1lem  47472  lighneallem3  47588  1arymaptfo  48590