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  7274  dfac9  10047  lediv12a  12035  leexp1a  14098  seqcoll  14387  lo1bdd2  15447  rlimcld2  15501  rlimcn1  15511  isercolllem1  15588  summo  15640  climcnds  15774  geomulcvg  15799  mertenslem2  15808  prodmolem2  15858  prodmo  15859  fprod2d  15904  pwsle  17413  isacs2  17576  grpinvalem  18598  gsumpropd2lem  18604  gsumwsubmcl  18762  gsumwmhm  18770  mulgfval  18999  gaid  19228  gsmsymgrfixlem1  19356  mulgnn0di  19754  gsumval3  19836  subrngint  20493  fvmptnn04if  22793  cnpnei  23208  lfinun  23469  xkopt  23599  isr0  23681  fbflim  23920  alexsubALTlem3  23993  metss  24452  iscmet3lem2  25248  ovoliunlem3  25461  mbfposr  25609  i1fmulclem  25659  itg10a  25667  iblss  25762  dvlip  25954  plyeq0lem  26171  mtest  26369  itgulm  26373  dchrisumlem3  27458  rpvmasum2  27479  pntlem3  27576  nosupbday  27673  noinfbday  27688  addonbday  28275  hlpasch  28828  f1otrg  28943  lfgrwlkprop  29759  wlkiswwlks1  29940  frgrnbnb  30368  frgr2wwlkeqm  30406  unidifsnne  32611  hashxpe  32887  ccatf1  33031  fxpsubm  33254  fxpsubrg  33256  mplvrpmmhm  33711  mplvrpmrhm  33712  vieta  33736  cos9thpiminplylem1  33939  signstfvneq0  34729  bnj605  35063  matunitlindflem1  37817  matunitlindflem2  37818  poimirlem26  37847  mblfinlem2  37859  ssfiunibd  45557  xralrple2  45599  infleinf  45616  infxrpnf  45690  fprodcn  45846  limsupub  45948  limsuppnflem  45954  limsupmnflem  45964  cnrefiisplem  46073  climxlim2lem  46089  icccncfext  46131  cncficcgt0  46132  cncfioobd  46141  dvbdfbdioolem2  46173  dvmptfprod  46189  itgspltprt  46223  stoweidlem34  46278  stoweidlem49  46293  stoweidlem57  46301  fourierdlem34  46385  fourierdlem39  46390  fourierdlem50  46400  fourierdlem51  46401  fourierdlem64  46414  fourierdlem73  46423  fourierdlem77  46427  fourierdlem81  46431  fourierdlem94  46444  fourierdlem97  46447  fourierdlem103  46453  fourierdlem104  46454  fourierdlem113  46463  fourier2  46471  etransclem24  46502  intsal  46574  sge0pr  46638  sge0iunmptlemfi  46657  sge0seq  46690  sge0reuz  46691  nnfoctbdjlem  46699  meadjiunlem  46709  ismeannd  46711  carageniuncllem2  46766  isomennd  46775  hoicvr  46792  hspmbllem2  46871  iunhoiioolem  46919  iunhoiioo  46920  vonioo  46926  vonicc  46929  preimageiingt  46964  preimaleiinlt  46965  smfaddlem1  47007  smfaddlem2  47008  smflimlem4  47018  smfrec  47033  smfinflem  47061  sprsymrelf1lem  47737  lighneallem3  47853  1arymaptfo  48889