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  759  ad5ant25  762  soisoi  7347  dfac9  10174  lediv12a  12158  leexp1a  14211  seqcoll  14499  lo1bdd2  15556  rlimcld2  15610  rlimcn1  15620  isercolllem1  15697  summo  15749  climcnds  15883  geomulcvg  15908  mertenslem2  15917  prodmolem2  15967  prodmo  15968  fprod2d  16013  pwsle  17538  isacs2  17697  grpinvalem  18698  gsumpropd2lem  18704  gsumwsubmcl  18862  gsumwmhm  18870  mulgfval  19099  gaid  19329  gsmsymgrfixlem1  19459  mulgnn0di  19857  gsumval3  19939  subrngint  20576  fvmptnn04if  22870  cnpnei  23287  lfinun  23548  xkopt  23678  isr0  23760  fbflim  23999  alexsubALTlem3  24072  metss  24536  iscmet3lem2  25339  ovoliunlem3  25552  mbfposr  25700  i1fmulclem  25751  itg10a  25759  iblss  25854  dvlip  26046  plyeq0lem  26263  mtest  26461  itgulm  26465  dchrisumlem3  27549  rpvmasum2  27570  pntlem3  27667  nosupbday  27764  noinfbday  27779  hlpasch  28778  f1otrg  28893  lfgrwlkprop  29719  wlkiswwlks1  29896  frgrnbnb  30321  frgr2wwlkeqm  30359  unidifsnne  32561  hashxpe  32816  ccatf1  32917  signstfvneq0  34565  bnj605  34899  matunitlindflem1  37602  matunitlindflem2  37603  poimirlem26  37632  mblfinlem2  37644  ssfiunibd  45259  xralrple2  45303  infleinf  45321  infxrpnf  45395  fprodcn  45555  limsupub  45659  limsuppnflem  45665  limsupmnflem  45675  cnrefiisplem  45784  climxlim2lem  45800  icccncfext  45842  cncficcgt0  45843  cncfioobd  45852  dvbdfbdioolem2  45884  dvmptfprod  45900  itgspltprt  45934  stoweidlem34  45989  stoweidlem49  46004  stoweidlem57  46012  fourierdlem34  46096  fourierdlem39  46101  fourierdlem50  46111  fourierdlem51  46112  fourierdlem64  46125  fourierdlem73  46134  fourierdlem77  46138  fourierdlem81  46142  fourierdlem94  46155  fourierdlem97  46158  fourierdlem103  46164  fourierdlem104  46165  fourierdlem113  46174  fourier2  46182  etransclem24  46213  intsal  46285  sge0pr  46349  sge0iunmptlemfi  46368  sge0seq  46401  sge0reuz  46402  nnfoctbdjlem  46410  meadjiunlem  46420  ismeannd  46422  carageniuncllem2  46477  isomennd  46486  hoicvr  46503  hspmbllem2  46582  iunhoiioolem  46630  iunhoiioo  46631  vonioo  46637  vonicc  46640  preimageiingt  46675  preimaleiinlt  46676  smfaddlem1  46718  smfaddlem2  46719  smflimlem4  46729  smfrec  46744  smfinflem  46772  sprsymrelf1lem  47415  lighneallem3  47531  1arymaptfo  48492