Theorem ad4ant14 765

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad5ant15  771  ad5ant25  774  ad5ant125  1390  soisoi  7334  dfac9  10208  lediv12a  12203  leexp1a  14311  seqcoll  14602  ccatf1  14729  lo1bdd2  15684  rlimcld2  15738  rlimcn1  15748  isercolllem1  15825  summo  15876  climcnds  16013  geomulcvg  16038  mertenslem2  16047  prodmolem2  16095  prodmo  16096  fprod2d  16141  pwsle  17657  isacs2  17820  grpinvalem  18847  gsumpropd2lem  18861  gsumwsubmcl  19026  gsumwmhm  19034  mulgfval  19272  gaid  19506  gsmsymgrfixlem1  19634  mulgnn0di  20032  gsumval3  20114  subrngint  20805  matunitlindflem1  22987  matunitlindflem2  22988  fvmptnn04if  23160  cnpnei  23575  lfinun  23837  xkopt  23967  isr0  24049  fbflim  24288  alexsubALTlem3  24361  metss  24820  iscmet3lem2  25606  ovoliunlem3  25818  mbfposr  25966  i1fmulclem  26016  itg10a  26024  iblss  26118  dvlip  26306  plyeq0lem  26522  mtest  26724  itgulm  26728  dchrisumlem3  27811  rpvmasum2  27832  pntlem3  27929  nosupbday  28055  noinfbday  28070  addonbday  28658  hlpasch  29227  f1otrg  29441  lfgrwlkprop  30263  wlkiswwlks1  30449  frgrnbnb  30887  frgr2wwlkeqm  30925  unidifsnne  33125  hashxpe  33392  fxpsubm  33726  fxpsubrg  33728  mplvrpmmhm  34171  mplvrpmrhm  34172  esplyfval1  34198  vieta  34205  cos9thpiminplylem1  34407  signstfvneq0  35194  bnj605  35530  poimirlem26  38544  mblfinlem2  38556  ssfiunibd  46294  xralrple2  46335  infleinf  46352  infxrpnf  46425  fprodcn  46581  limsupub  46683  limsuppnflem  46689  limsupmnflem  46699  cnrefiisplem  46808  climxlim2lem  46824  icccncfext  46866  cncficcgt0  46867  cncfioobd  46876  dvbdfbdioolem2  46908  dvmptfprod  46924  itgspltprt  46958  stoweidlem34  47013  stoweidlem49  47028  stoweidlem57  47036  fourierdlem34  47120  fourierdlem39  47125  fourierdlem50  47135  fourierdlem51  47136  fourierdlem64  47149  fourierdlem73  47158  fourierdlem77  47162  fourierdlem81  47166  fourierdlem94  47179  fourierdlem97  47182  fourierdlem103  47188  fourierdlem104  47189  fourierdlem113  47198  fourier2  47206  etransclem24  47237  intsal  47309  sge0pr  47373  sge0iunmptlemfi  47392  sge0seq  47425  sge0reuz  47426  nnfoctbdjlem  47434  meadjiunlem  47444  ismeannd  47446  carageniuncllem2  47501  isomennd  47510  hoicvr  47527  hspmbllem2  47606  iunhoiioolem  47654  iunhoiioo  47655  vonioo  47661  vonicc  47664  preimageiingt  47699  preimaleiinlt  47700  smfaddlem1  47742  smfaddlem2  47743  smflimlem4  47753  smfrec  47768  smfinflem  47796  sprsymrelf1lem  48542  lighneallem3  48661  1arymaptfo  49724