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  7335  dfac9  10136  lediv12a  12123  leexp1a  14229  seqcoll  14519  ccatf1  14646  lo1bdd2  15599  rlimcld2  15653  rlimcn1  15663  isercolllem1  15740  summo  15791  climcnds  15928  geomulcvg  15953  mertenslem2  15962  prodmolem2  16012  prodmo  16013  fprod2d  16058  pwsle  17568  isacs2  17731  grpinvalem  18757  gsumpropd2lem  18769  gsumwsubmcl  18933  gsumwmhm  18941  mulgfval  19179  gaid  19413  gsmsymgrfixlem1  19541  mulgnn0di  19939  gsumval3  20021  subrngint  20709  fvmptnn04if  23056  cnpnei  23471  lfinun  23733  xkopt  23863  isr0  23945  fbflim  24184  alexsubALTlem3  24257  metss  24716  iscmet3lem2  25502  ovoliunlem3  25714  mbfposr  25862  i1fmulclem  25912  itg10a  25920  iblss  26015  dvlip  26203  plyeq0lem  26418  mtest  26618  itgulm  26622  dchrisumlem3  27706  rpvmasum2  27727  pntlem3  27824  nosupbday  27920  noinfbday  27935  addonbday  28523  hlpasch  29089  f1otrg  29275  lfgrwlkprop  30097  wlkiswwlks1  30283  frgrnbnb  30715  frgr2wwlkeqm  30753  unidifsnne  32953  hashxpe  33222  fxpsubm  33556  fxpsubrg  33558  mplvrpmmhm  34000  mplvrpmrhm  34001  esplyfval1  34027  vieta  34034  cos9thpiminplylem1  34236  signstfvneq0  35024  bnj605  35360  matunitlindflem1  38324  matunitlindflem2  38325  poimirlem26  38354  mblfinlem2  38366  ssfiunibd  46086  xralrple2  46128  infleinf  46145  infxrpnf  46218  fprodcn  46374  limsupub  46476  limsuppnflem  46482  limsupmnflem  46492  cnrefiisplem  46601  climxlim2lem  46617  icccncfext  46659  cncficcgt0  46660  cncfioobd  46669  dvbdfbdioolem2  46701  dvmptfprod  46717  itgspltprt  46751  stoweidlem34  46806  stoweidlem49  46821  stoweidlem57  46829  fourierdlem34  46913  fourierdlem39  46918  fourierdlem50  46928  fourierdlem51  46929  fourierdlem64  46942  fourierdlem73  46951  fourierdlem77  46955  fourierdlem81  46959  fourierdlem94  46972  fourierdlem97  46975  fourierdlem103  46981  fourierdlem104  46982  fourierdlem113  46991  fourier2  46999  etransclem24  47030  intsal  47102  sge0pr  47166  sge0iunmptlemfi  47185  sge0seq  47218  sge0reuz  47219  nnfoctbdjlem  47227  meadjiunlem  47237  ismeannd  47239  carageniuncllem2  47294  isomennd  47303  hoicvr  47320  hspmbllem2  47399  iunhoiioolem  47447  iunhoiioo  47448  vonioo  47454  vonicc  47457  preimageiingt  47492  preimaleiinlt  47493  smfaddlem1  47535  smfaddlem2  47536  smflimlem4  47546  smfrec  47561  smfinflem  47589  sprsymrelf1lem  48298  lighneallem3  48417  1arymaptfo  49480