Theorem ad4ant14 764

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad5ant15  770  ad5ant25  773  ad5ant125  1390  soisoi  7326  dfac9  10116  lediv12a  12103  leexp1a  14207  seqcoll  14497  lo1bdd2  15571  rlimcld2  15625  rlimcn1  15635  isercolllem1  15712  summo  15764  climcnds  15901  geomulcvg  15926  mertenslem2  15935  prodmolem2  15985  prodmo  15986  fprod2d  16031  pwsle  17541  isacs2  17704  grpinvalem  18726  gsumpropd2lem  18732  gsumwsubmcl  18891  gsumwmhm  18899  mulgfval  19130  gaid  19364  gsmsymgrfixlem1  19492  mulgnn0di  19890  gsumval3  19972  subrngint  20659  fvmptnn04if  23006  cnpnei  23421  lfinun  23682  xkopt  23812  isr0  23894  fbflim  24133  alexsubALTlem3  24206  metss  24665  iscmet3lem2  25451  ovoliunlem3  25663  mbfposr  25811  i1fmulclem  25861  itg10a  25869  iblss  25964  dvlip  26152  plyeq0lem  26367  mtest  26567  itgulm  26571  dchrisumlem3  27655  rpvmasum2  27676  pntlem3  27773  nosupbday  27869  noinfbday  27884  addonbday  28472  hlpasch  29038  f1otrg  29220  lfgrwlkprop  30035  wlkiswwlks1  30216  frgrnbnb  30644  frgr2wwlkeqm  30682  unidifsnne  32882  hashxpe  33152  ccatf1  33269  fxpsubm  33492  fxpsubrg  33494  mplvrpmmhm  33936  mplvrpmrhm  33937  esplyfval1  33963  vieta  33970  cos9thpiminplylem1  34172  signstfvneq0  34959  bnj605  35295  matunitlindflem1  38267  matunitlindflem2  38268  poimirlem26  38297  mblfinlem2  38309  ssfiunibd  46028  xralrple2  46070  infleinf  46087  infxrpnf  46160  fprodcn  46316  limsupub  46418  limsuppnflem  46424  limsupmnflem  46434  cnrefiisplem  46543  climxlim2lem  46559  icccncfext  46601  cncficcgt0  46602  cncfioobd  46611  dvbdfbdioolem2  46643  dvmptfprod  46659  itgspltprt  46693  stoweidlem34  46748  stoweidlem49  46763  stoweidlem57  46771  fourierdlem34  46855  fourierdlem39  46860  fourierdlem50  46870  fourierdlem51  46871  fourierdlem64  46884  fourierdlem73  46893  fourierdlem77  46897  fourierdlem81  46901  fourierdlem94  46914  fourierdlem97  46917  fourierdlem103  46923  fourierdlem104  46924  fourierdlem113  46933  fourier2  46941  etransclem24  46972  intsal  47044  sge0pr  47108  sge0iunmptlemfi  47127  sge0seq  47160  sge0reuz  47161  nnfoctbdjlem  47169  meadjiunlem  47179  ismeannd  47181  carageniuncllem2  47236  isomennd  47245  hoicvr  47262  hspmbllem2  47341  iunhoiioolem  47389  iunhoiioo  47390  vonioo  47396  vonicc  47399  preimageiingt  47434  preimaleiinlt  47435  smfaddlem1  47477  smfaddlem2  47478  smflimlem4  47488  smfrec  47503  smfinflem  47531  sprsymrelf1lem  48240  lighneallem3  48359  1arymaptfo  49423