Theorem ad4ant14 762

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  ad5ant15  768  ad5ant25  771  ad5ant125  1382  soisoi  7312  dfac9  10093  lediv12a  12085  leexp1a  14188  seqcoll  14477  lo1bdd2  15551  rlimcld2  15605  rlimcn1  15615  isercolllem1  15692  summo  15744  climcnds  15881  geomulcvg  15906  mertenslem2  15915  prodmolem2  15965  prodmo  15966  fprod2d  16011  pwsle  17522  isacs2  17685  grpinvalem  18707  gsumpropd2lem  18713  gsumwsubmcl  18871  gsumwmhm  18879  mulgfval  19111  gaid  19339  gsmsymgrfixlem1  19467  mulgnn0di  19865  gsumval3  19947  subrngint  20606  fvmptnn04if  22906  cnpnei  23321  lfinun  23582  xkopt  23712  isr0  23794  fbflim  24033  alexsubALTlem3  24106  metss  24565  iscmet3lem2  25351  ovoliunlem3  25563  mbfposr  25711  i1fmulclem  25761  itg10a  25769  iblss  25864  dvlip  26052  plyeq0lem  26267  mtest  26464  itgulm  26468  dchrisumlem3  27552  rpvmasum2  27573  pntlem3  27670  nosupbday  27766  noinfbday  27781  addonbday  28369  hlpasch  28926  f1otrg  29068  lfgrwlkprop  29883  wlkiswwlks1  30064  frgrnbnb  30492  frgr2wwlkeqm  30530  unidifsnne  32732  hashxpe  33006  ccatf1  33124  fxpsubm  33349  fxpsubrg  33351  mplvrpmmhm  33840  mplvrpmrhm  33841  esplyfval1  33867  vieta  33874  cos9thpiminplylem1  34076  signstfvneq0  34863  bnj605  35199  matunitlindflem1  38112  matunitlindflem2  38113  poimirlem26  38142  mblfinlem2  38154  ssfiunibd  45885  xralrple2  45927  infleinf  45944  infxrpnf  46017  fprodcn  46173  limsupub  46275  limsuppnflem  46281  limsupmnflem  46291  cnrefiisplem  46400  climxlim2lem  46416  icccncfext  46458  cncficcgt0  46459  cncfioobd  46468  dvbdfbdioolem2  46500  dvmptfprod  46516  itgspltprt  46550  stoweidlem34  46605  stoweidlem49  46620  stoweidlem57  46628  fourierdlem34  46712  fourierdlem39  46717  fourierdlem50  46727  fourierdlem51  46728  fourierdlem64  46741  fourierdlem73  46750  fourierdlem77  46754  fourierdlem81  46758  fourierdlem94  46771  fourierdlem97  46774  fourierdlem103  46780  fourierdlem104  46781  fourierdlem113  46790  fourier2  46798  etransclem24  46829  intsal  46901  sge0pr  46965  sge0iunmptlemfi  46984  sge0seq  47017  sge0reuz  47018  nnfoctbdjlem  47026  meadjiunlem  47036  ismeannd  47038  carageniuncllem2  47093  isomennd  47102  hoicvr  47119  hspmbllem2  47198  iunhoiioolem  47246  iunhoiioo  47247  vonioo  47253  vonicc  47256  preimageiingt  47291  preimaleiinlt  47292  smfaddlem1  47334  smfaddlem2  47335  smflimlem4  47345  smfrec  47360  smfinflem  47388  sprsymrelf1lem  48094  lighneallem3  48213  1arymaptfo  49262