Theorem ad4ant14 749

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  ad5ant15  756  ad5ant25  759  soisoi  7208  dfac9  9901  lediv12a  11877  leexp1a  13902  seqcoll  14187  lo1bdd2  15242  rlimcld2  15296  rlimcn1  15306  isercolllem1  15385  summo  15438  climcnds  15572  geomulcvg  15597  mertenslem2  15606  prodmolem2  15654  prodmo  15655  fprod2d  15700  pwsle  17212  isacs2  17371  grprinvlem  18366  gsumpropd2lem  18372  gsumwsubmcl  18484  gsumwmhm  18493  mulgfval  18711  gaid  18914  gsmsymgrfixlem1  19044  mulgnn0di  19436  gsumval3  19517  fvmptnn04if  22007  cnpnei  22424  lfinun  22685  xkopt  22815  isr0  22897  fbflim  23136  alexsubALTlem3  23209  metss  23673  iscmet3lem2  24465  ovoliunlem3  24677  mbfposr  24825  i1fmulclem  24876  itg10a  24884  iblss  24978  dvlip  25166  plyeq0lem  25380  mtest  25572  itgulm  25576  dchrisumlem3  26648  rpvmasum2  26669  pntlem3  26766  hlpasch  27126  f1otrg  27241  lfgrwlkprop  28064  wlkiswwlks1  28241  frgrnbnb  28666  frgr2wwlkeqm  28704  unidifsnne  30893  hashxpe  31136  ccatf1  31232  signstfvneq0  32560  bnj605  32896  nosupbday  33917  noinfbday  33932  matunitlindflem1  35782  matunitlindflem2  35783  poimirlem26  35812  mblfinlem2  35824  ssfiunibd  42855  xralrple2  42900  infleinf  42918  infxrpnf  42993  fprodcn  43148  limsupub  43252  limsuppnflem  43258  limsupmnflem  43268  cnrefiisplem  43377  climxlim2lem  43393  icccncfext  43435  cncficcgt0  43436  cncfioobd  43445  dvbdfbdioolem2  43477  itgspltprt  43527  stoweidlem34  43582  stoweidlem49  43597  stoweidlem57  43605  fourierdlem34  43689  fourierdlem39  43694  fourierdlem50  43704  fourierdlem51  43705  fourierdlem64  43718  fourierdlem73  43727  fourierdlem77  43731  fourierdlem81  43735  fourierdlem94  43748  fourierdlem97  43751  fourierdlem103  43757  fourierdlem104  43758  fourierdlem113  43767  fourier2  43775  etransclem24  43806  intsal  43876  sge0pr  43939  sge0iunmptlemfi  43958  sge0seq  43991  sge0reuz  43992  nnfoctbdjlem  44000  meadjiunlem  44010  ismeannd  44012  carageniuncllem2  44067  isomennd  44076  hoicvr  44093  hspmbllem2  44172  iunhoiioolem  44220  iunhoiioo  44221  vonioo  44227  vonicc  44230  preimageiingt  44265  preimaleiinlt  44266  smfaddlem1  44308  smfaddlem2  44309  smflimlem4  44319  smfrec  44334  smfinflem  44361  sprsymrelf1lem  44954  lighneallem3  45070  isomgreqve  45288  1arymaptfo  46000