Theorem ad4ant14 739

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  ad5ant15  746  ad5ant25  749  soisoi  6904  grprinvlem  7202  dfac9  9356  lediv12a  11334  leexp1a  13354  seqcoll  13635  lo1bdd2  14742  rlimcld2  14796  rlimcn1  14806  isercolllem1  14882  summo  14934  climcnds  15066  geomulcvg  15092  mertenslem2  15101  prodmolem2  15149  prodmo  15150  fprod2d  15195  pwsle  16621  isacs2  16782  gsumpropd2lem  17741  gsumwsubmcl  17843  gsumwmhm  17851  mulgfval  18013  gaid  18200  mulgnn0di  18704  gsumval3  18781  fvmptnn04if  21161  cnpnei  21576  lfinun  21837  xkopt  21967  isr0  22049  fbflim  22288  alexsubALTlem3  22361  metss  22821  iscmet3lem2  23598  ovoliunlem3  23808  mbfposr  23956  i1fmulclem  24006  itg10a  24014  iblss  24108  dvlip  24293  plyeq0lem  24503  mtest  24695  itgulm  24699  dchrisumlem3  25769  rpvmasum2  25790  pntlem3  25887  hlpasch  26244  f1otrg  26360  lfgrwlkprop  27175  wlkiswwlks1  27353  frgrnbnb  27827  frgr2wwlkeqm  27865  hashxpe  30276  bnj605  31823  matunitlindflem1  34326  matunitlindflem2  34327  poimirlem26  34356  mblfinlem2  34368  ssfiunibd  41003  xralrple2  41049  infleinf  41067  infxrpnf  41150  fprodcn  41310  limsupub  41414  limsuppnflem  41420  limsupmnflem  41430  cnrefiisplem  41539  climxlim2lem  41555  icccncfext  41598  cncficcgt0  41599  cncfioobd  41608  dvbdfbdioolem2  41642  itgspltprt  41692  stoweidlem34  41748  stoweidlem49  41763  stoweidlem57  41771  fourierdlem34  41855  fourierdlem39  41860  fourierdlem50  41870  fourierdlem51  41871  fourierdlem64  41884  fourierdlem73  41893  fourierdlem77  41897  fourierdlem81  41901  fourierdlem94  41914  fourierdlem97  41917  fourierdlem103  41923  fourierdlem104  41924  fourierdlem113  41933  fourier2  41941  etransclem24  41972  intsal  42042  sge0pr  42105  sge0iunmptlemfi  42124  sge0seq  42157  sge0reuz  42158  nnfoctbdjlem  42166  meadjiunlem  42176  ismeannd  42178  carageniuncllem2  42233  isomennd  42242  hoicvr  42259  hspmbllem2  42338  iunhoiioolem  42386  iunhoiioo  42387  vonioo  42393  vonicc  42396  preimageiingt  42427  preimaleiinlt  42428  smfaddlem1  42468  smfaddlem2  42469  smflimlem4  42479  smfrec  42493  smfinflem  42520  sprsymrelf1lem  43019  lighneallem3  43138  isomgreqve  43356