Theorem ad4ant14 758

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ad5ant15  764  ad5ant25  767  soisoi  7272  dfac9  10050  lediv12a  12040  leexp1a  14128  seqcoll  14417  lo1bdd2  15477  rlimcld2  15531  rlimcn1  15541  isercolllem1  15618  summo  15670  climcnds  15807  geomulcvg  15832  mertenslem2  15841  prodmolem2  15891  prodmo  15892  fprod2d  15937  pwsle  17447  isacs2  17610  grpinvalem  18632  gsumpropd2lem  18638  gsumwsubmcl  18796  gsumwmhm  18804  mulgfval  19036  gaid  19265  gsmsymgrfixlem1  19393  mulgnn0di  19791  gsumval3  19873  subrngint  20532  fvmptnn04if  22832  cnpnei  23247  lfinun  23508  xkopt  23638  isr0  23720  fbflim  23959  alexsubALTlem3  24032  metss  24491  iscmet3lem2  25277  ovoliunlem3  25489  mbfposr  25637  i1fmulclem  25687  itg10a  25695  iblss  25790  dvlip  25978  plyeq0lem  26193  mtest  26387  itgulm  26391  dchrisumlem3  27472  rpvmasum2  27493  pntlem3  27590  nosupbday  27687  noinfbday  27702  addonbday  28289  hlpasch  28842  f1otrg  28957  lfgrwlkprop  29772  wlkiswwlks1  29953  frgrnbnb  30381  frgr2wwlkeqm  30419  unidifsnne  32624  hashxpe  32899  ccatf1  33028  fxpsubm  33253  fxpsubrg  33255  mplvrpmmhm  33730  mplvrpmrhm  33731  esplyfval1  33757  vieta  33764  cos9thpiminplylem1  33966  signstfvneq0  34756  bnj605  35089  matunitlindflem1  37983  matunitlindflem2  37984  poimirlem26  38013  mblfinlem2  38025  ssfiunibd  45757  xralrple2  45799  infleinf  45816  infxrpnf  45889  fprodcn  46045  limsupub  46147  limsuppnflem  46153  limsupmnflem  46163  cnrefiisplem  46272  climxlim2lem  46288  icccncfext  46330  cncficcgt0  46331  cncfioobd  46340  dvbdfbdioolem2  46372  dvmptfprod  46388  itgspltprt  46422  stoweidlem34  46477  stoweidlem49  46492  stoweidlem57  46500  fourierdlem34  46584  fourierdlem39  46589  fourierdlem50  46599  fourierdlem51  46600  fourierdlem64  46613  fourierdlem73  46622  fourierdlem77  46626  fourierdlem81  46630  fourierdlem94  46643  fourierdlem97  46646  fourierdlem103  46652  fourierdlem104  46653  fourierdlem113  46662  fourier2  46670  etransclem24  46701  intsal  46773  sge0pr  46837  sge0iunmptlemfi  46856  sge0seq  46889  sge0reuz  46890  nnfoctbdjlem  46898  meadjiunlem  46908  ismeannd  46910  carageniuncllem2  46965  isomennd  46974  hoicvr  46991  hspmbllem2  47070  iunhoiioolem  47118  iunhoiioo  47119  vonioo  47125  vonicc  47128  preimageiingt  47163  preimaleiinlt  47164  smfaddlem1  47206  smfaddlem2  47207  smflimlem4  47217  smfrec  47232  smfinflem  47260  sprsymrelf1lem  47966  lighneallem3  48085  1arymaptfo  49134