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  759  ad5ant25  762  soisoi  7348  dfac9  10177  lediv12a  12161  leexp1a  14215  seqcoll  14503  lo1bdd2  15560  rlimcld2  15614  rlimcn1  15624  isercolllem1  15701  summo  15753  climcnds  15887  geomulcvg  15912  mertenslem2  15921  prodmolem2  15971  prodmo  15972  fprod2d  16017  pwsle  17537  isacs2  17696  grpinvalem  18686  gsumpropd2lem  18692  gsumwsubmcl  18850  gsumwmhm  18858  mulgfval  19087  gaid  19317  gsmsymgrfixlem1  19445  mulgnn0di  19843  gsumval3  19925  subrngint  20560  fvmptnn04if  22855  cnpnei  23272  lfinun  23533  xkopt  23663  isr0  23745  fbflim  23984  alexsubALTlem3  24057  metss  24521  iscmet3lem2  25326  ovoliunlem3  25539  mbfposr  25687  i1fmulclem  25737  itg10a  25745  iblss  25840  dvlip  26032  plyeq0lem  26249  mtest  26447  itgulm  26451  dchrisumlem3  27535  rpvmasum2  27556  pntlem3  27653  nosupbday  27750  noinfbday  27765  hlpasch  28764  f1otrg  28879  lfgrwlkprop  29705  wlkiswwlks1  29887  frgrnbnb  30312  frgr2wwlkeqm  30350  unidifsnne  32554  hashxpe  32811  ccatf1  32933  signstfvneq0  34587  bnj605  34921  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem26  37653  mblfinlem2  37665  ssfiunibd  45321  xralrple2  45365  infleinf  45383  infxrpnf  45457  fprodcn  45615  limsupub  45719  limsuppnflem  45725  limsupmnflem  45735  cnrefiisplem  45844  climxlim2lem  45860  icccncfext  45902  cncficcgt0  45903  cncfioobd  45912  dvbdfbdioolem2  45944  dvmptfprod  45960  itgspltprt  45994  stoweidlem34  46049  stoweidlem49  46064  stoweidlem57  46072  fourierdlem34  46156  fourierdlem39  46161  fourierdlem50  46171  fourierdlem51  46172  fourierdlem64  46185  fourierdlem73  46194  fourierdlem77  46198  fourierdlem81  46202  fourierdlem94  46215  fourierdlem97  46218  fourierdlem103  46224  fourierdlem104  46225  fourierdlem113  46234  fourier2  46242  etransclem24  46273  intsal  46345  sge0pr  46409  sge0iunmptlemfi  46428  sge0seq  46461  sge0reuz  46462  nnfoctbdjlem  46470  meadjiunlem  46480  ismeannd  46482  carageniuncllem2  46537  isomennd  46546  hoicvr  46563  hspmbllem2  46642  iunhoiioolem  46690  iunhoiioo  46691  vonioo  46697  vonicc  46700  preimageiingt  46735  preimaleiinlt  46736  smfaddlem1  46778  smfaddlem2  46779  smflimlem4  46789  smfrec  46804  smfinflem  46832  sprsymrelf1lem  47478  lighneallem3  47594  1arymaptfo  48564