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  758  ad5ant25  761  soisoi  7265  dfac9  10031  lediv12a  12018  leexp1a  14082  seqcoll  14371  lo1bdd2  15431  rlimcld2  15485  rlimcn1  15495  isercolllem1  15572  summo  15624  climcnds  15758  geomulcvg  15783  mertenslem2  15792  prodmolem2  15842  prodmo  15843  fprod2d  15888  pwsle  17396  isacs2  17559  grpinvalem  18547  gsumpropd2lem  18553  gsumwsubmcl  18711  gsumwmhm  18719  mulgfval  18948  gaid  19178  gsmsymgrfixlem1  19306  mulgnn0di  19704  gsumval3  19786  subrngint  20445  fvmptnn04if  22734  cnpnei  23149  lfinun  23410  xkopt  23540  isr0  23622  fbflim  23861  alexsubALTlem3  23934  metss  24394  iscmet3lem2  25190  ovoliunlem3  25403  mbfposr  25551  i1fmulclem  25601  itg10a  25609  iblss  25704  dvlip  25896  plyeq0lem  26113  mtest  26311  itgulm  26315  dchrisumlem3  27400  rpvmasum2  27421  pntlem3  27518  nosupbday  27615  noinfbday  27630  hlpasch  28701  f1otrg  28816  lfgrwlkprop  29631  wlkiswwlks1  29812  frgrnbnb  30237  frgr2wwlkeqm  30275  unidifsnne  32480  hashxpe  32752  ccatf1  32890  fxpsubm  33114  fxpsubrg  33116  cos9thpiminplylem1  33749  signstfvneq0  34540  bnj605  34874  matunitlindflem1  37596  matunitlindflem2  37597  poimirlem26  37626  mblfinlem2  37638  ssfiunibd  45291  xralrple2  45334  infleinf  45351  infxrpnf  45425  fprodcn  45581  limsupub  45685  limsuppnflem  45691  limsupmnflem  45701  cnrefiisplem  45810  climxlim2lem  45826  icccncfext  45868  cncficcgt0  45869  cncfioobd  45878  dvbdfbdioolem2  45910  dvmptfprod  45926  itgspltprt  45960  stoweidlem34  46015  stoweidlem49  46030  stoweidlem57  46038  fourierdlem34  46122  fourierdlem39  46127  fourierdlem50  46137  fourierdlem51  46138  fourierdlem64  46151  fourierdlem73  46160  fourierdlem77  46164  fourierdlem81  46168  fourierdlem94  46181  fourierdlem97  46184  fourierdlem103  46190  fourierdlem104  46191  fourierdlem113  46200  fourier2  46208  etransclem24  46239  intsal  46311  sge0pr  46375  sge0iunmptlemfi  46394  sge0seq  46427  sge0reuz  46428  nnfoctbdjlem  46436  meadjiunlem  46446  ismeannd  46448  carageniuncllem2  46503  isomennd  46512  hoicvr  46529  hspmbllem2  46608  iunhoiioolem  46656  iunhoiioo  46657  vonioo  46663  vonicc  46666  preimageiingt  46701  preimaleiinlt  46702  smfaddlem1  46744  smfaddlem2  46745  smflimlem4  46755  smfrec  46770  smfinflem  46798  sprsymrelf1lem  47475  lighneallem3  47591  1arymaptfo  48628