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  7262  dfac9  10028  lediv12a  12015  leexp1a  14082  seqcoll  14371  lo1bdd2  15431  rlimcld2  15485  rlimcn1  15495  isercolllem1  15572  summo  15624  climcnds  15758  geomulcvg  15783  mertenslem2  15792  prodmolem2  15842  prodmo  15843  fprod2d  15888  pwsle  17396  isacs2  17559  grpinvalem  18581  gsumpropd2lem  18587  gsumwsubmcl  18745  gsumwmhm  18753  mulgfval  18982  gaid  19211  gsmsymgrfixlem1  19339  mulgnn0di  19737  gsumval3  19819  subrngint  20475  fvmptnn04if  22764  cnpnei  23179  lfinun  23440  xkopt  23570  isr0  23652  fbflim  23891  alexsubALTlem3  23964  metss  24423  iscmet3lem2  25219  ovoliunlem3  25432  mbfposr  25580  i1fmulclem  25630  itg10a  25638  iblss  25733  dvlip  25925  plyeq0lem  26142  mtest  26340  itgulm  26344  dchrisumlem3  27429  rpvmasum2  27450  pntlem3  27547  nosupbday  27644  noinfbday  27659  hlpasch  28734  f1otrg  28849  lfgrwlkprop  29664  wlkiswwlks1  29845  frgrnbnb  30273  frgr2wwlkeqm  30311  unidifsnne  32516  hashxpe  32789  ccatf1  32930  fxpsubm  33141  fxpsubrg  33143  mplvrpmmhm  33576  mplvrpmrhm  33577  cos9thpiminplylem1  33795  signstfvneq0  34585  bnj605  34919  matunitlindflem1  37655  matunitlindflem2  37656  poimirlem26  37685  mblfinlem2  37697  ssfiunibd  45409  xralrple2  45452  infleinf  45469  infxrpnf  45543  fprodcn  45699  limsupub  45801  limsuppnflem  45807  limsupmnflem  45817  cnrefiisplem  45926  climxlim2lem  45942  icccncfext  45984  cncficcgt0  45985  cncfioobd  45994  dvbdfbdioolem2  46026  dvmptfprod  46042  itgspltprt  46076  stoweidlem34  46131  stoweidlem49  46146  stoweidlem57  46154  fourierdlem34  46238  fourierdlem39  46243  fourierdlem50  46253  fourierdlem51  46254  fourierdlem64  46267  fourierdlem73  46276  fourierdlem77  46280  fourierdlem81  46284  fourierdlem94  46297  fourierdlem97  46300  fourierdlem103  46306  fourierdlem104  46307  fourierdlem113  46316  fourier2  46324  etransclem24  46355  intsal  46427  sge0pr  46491  sge0iunmptlemfi  46510  sge0seq  46543  sge0reuz  46544  nnfoctbdjlem  46552  meadjiunlem  46562  ismeannd  46564  carageniuncllem2  46619  isomennd  46628  hoicvr  46645  hspmbllem2  46724  iunhoiioolem  46772  iunhoiioo  46773  vonioo  46779  vonicc  46782  preimageiingt  46817  preimaleiinlt  46818  smfaddlem1  46860  smfaddlem2  46861  smflimlem4  46871  smfrec  46886  smfinflem  46914  sprsymrelf1lem  47590  lighneallem3  47706  1arymaptfo  48743