Theorem ad4ant14 751

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 714	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	adantlr 714	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  758  ad5ant25  761  soisoi  7364  dfac9  10206  lediv12a  12188  leexp1a  14225  seqcoll  14513  lo1bdd2  15570  rlimcld2  15624  rlimcn1  15634  isercolllem1  15713  summo  15765  climcnds  15899  geomulcvg  15924  mertenslem2  15933  prodmolem2  15983  prodmo  15984  fprod2d  16029  pwsle  17552  isacs2  17711  grpinvalem  18711  gsumpropd2lem  18717  gsumwsubmcl  18872  gsumwmhm  18880  mulgfval  19109  gaid  19339  gsmsymgrfixlem1  19469  mulgnn0di  19867  gsumval3  19949  subrngint  20586  fvmptnn04if  22876  cnpnei  23293  lfinun  23554  xkopt  23684  isr0  23766  fbflim  24005  alexsubALTlem3  24078  metss  24542  iscmet3lem2  25345  ovoliunlem3  25558  mbfposr  25706  i1fmulclem  25757  itg10a  25765  iblss  25860  dvlip  26052  plyeq0lem  26269  mtest  26465  itgulm  26469  dchrisumlem3  27553  rpvmasum2  27574  pntlem3  27671  nosupbday  27768  noinfbday  27783  hlpasch  28782  f1otrg  28897  lfgrwlkprop  29723  wlkiswwlks1  29900  frgrnbnb  30325  frgr2wwlkeqm  30363  unidifsnne  32564  hashxpe  32814  ccatf1  32915  signstfvneq0  34549  bnj605  34883  matunitlindflem1  37576  matunitlindflem2  37577  poimirlem26  37606  mblfinlem2  37618  ssfiunibd  45224  xralrple2  45269  infleinf  45287  infxrpnf  45361  fprodcn  45521  limsupub  45625  limsuppnflem  45631  limsupmnflem  45641  cnrefiisplem  45750  climxlim2lem  45766  icccncfext  45808  cncficcgt0  45809  cncfioobd  45818  dvbdfbdioolem2  45850  itgspltprt  45900  stoweidlem34  45955  stoweidlem49  45970  stoweidlem57  45978  fourierdlem34  46062  fourierdlem39  46067  fourierdlem50  46077  fourierdlem51  46078  fourierdlem64  46091  fourierdlem73  46100  fourierdlem77  46104  fourierdlem81  46108  fourierdlem94  46121  fourierdlem97  46124  fourierdlem103  46130  fourierdlem104  46131  fourierdlem113  46140  fourier2  46148  etransclem24  46179  intsal  46251  sge0pr  46315  sge0iunmptlemfi  46334  sge0seq  46367  sge0reuz  46368  nnfoctbdjlem  46376  meadjiunlem  46386  ismeannd  46388  carageniuncllem2  46443  isomennd  46452  hoicvr  46469  hspmbllem2  46548  iunhoiioolem  46596  iunhoiioo  46597  vonioo  46603  vonicc  46606  preimageiingt  46641  preimaleiinlt  46642  smfaddlem1  46684  smfaddlem2  46685  smflimlem4  46695  smfrec  46710  smfinflem  46738  sprsymrelf1lem  47365  lighneallem3  47481  1arymaptfo  48377