Theorem ad4ant14 751

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 714	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	adantlr 714	1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  ad5ant15  758  ad5ant25  761  soisoi  7325  dfac9  10131  lediv12a  12107  leexp1a  14140  seqcoll  14425  lo1bdd2  15468  rlimcld2  15522  rlimcn1  15532  isercolllem1  15611  summo  15663  climcnds  15797  geomulcvg  15822  mertenslem2  15831  prodmolem2  15879  prodmo  15880  fprod2d  15925  pwsle  17438  isacs2  17597  grprinvlem  18592  gsumpropd2lem  18598  gsumwsubmcl  18718  gsumwmhm  18726  mulgfval  18952  gaid  19163  gsmsymgrfixlem1  19295  mulgnn0di  19693  gsumval3  19775  fvmptnn04if  22351  cnpnei  22768  lfinun  23029  xkopt  23159  isr0  23241  fbflim  23480  alexsubALTlem3  23553  metss  24017  iscmet3lem2  24809  ovoliunlem3  25021  mbfposr  25169  i1fmulclem  25220  itg10a  25228  iblss  25322  dvlip  25510  plyeq0lem  25724  mtest  25916  itgulm  25920  dchrisumlem3  26994  rpvmasum2  27015  pntlem3  27112  nosupbday  27208  noinfbday  27223  hlpasch  28007  f1otrg  28122  lfgrwlkprop  28944  wlkiswwlks1  29121  frgrnbnb  29546  frgr2wwlkeqm  29584  unidifsnne  31773  hashxpe  32019  ccatf1  32115  signstfvneq0  33583  bnj605  33918  matunitlindflem1  36484  matunitlindflem2  36485  poimirlem26  36514  mblfinlem2  36526  ssfiunibd  44019  xralrple2  44064  infleinf  44082  infxrpnf  44156  fprodcn  44316  limsupub  44420  limsuppnflem  44426  limsupmnflem  44436  cnrefiisplem  44545  climxlim2lem  44561  icccncfext  44603  cncficcgt0  44604  cncfioobd  44613  dvbdfbdioolem2  44645  itgspltprt  44695  stoweidlem34  44750  stoweidlem49  44765  stoweidlem57  44773  fourierdlem34  44857  fourierdlem39  44862  fourierdlem50  44872  fourierdlem51  44873  fourierdlem64  44886  fourierdlem73  44895  fourierdlem77  44899  fourierdlem81  44903  fourierdlem94  44916  fourierdlem97  44919  fourierdlem103  44925  fourierdlem104  44926  fourierdlem113  44935  fourier2  44943  etransclem24  44974  intsal  45046  sge0pr  45110  sge0iunmptlemfi  45129  sge0seq  45162  sge0reuz  45163  nnfoctbdjlem  45171  meadjiunlem  45181  ismeannd  45183  carageniuncllem2  45238  isomennd  45247  hoicvr  45264  hspmbllem2  45343  iunhoiioolem  45391  iunhoiioo  45392  vonioo  45398  vonicc  45401  preimageiingt  45436  preimaleiinlt  45437  smfaddlem1  45479  smfaddlem2  45480  smflimlem4  45490  smfrec  45505  smfinflem  45533  sprsymrelf1lem  46159  lighneallem3  46275  isomgreqve  46493  subrngint  46739  1arymaptfo  47329