Theorem ad4ant14 750

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 713	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	adantlr 713	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  757  ad5ant25  760  soisoi  7327  dfac9  10133  lediv12a  12109  leexp1a  14142  seqcoll  14427  lo1bdd2  15470  rlimcld2  15524  rlimcn1  15534  isercolllem1  15613  summo  15665  climcnds  15799  geomulcvg  15824  mertenslem2  15833  prodmolem2  15881  prodmo  15882  fprod2d  15927  pwsle  17440  isacs2  17599  grprinvlem  18594  gsumpropd2lem  18600  gsumwsubmcl  18720  gsumwmhm  18728  mulgfval  18954  gaid  19165  gsmsymgrfixlem1  19297  mulgnn0di  19695  gsumval3  19777  fvmptnn04if  22358  cnpnei  22775  lfinun  23036  xkopt  23166  isr0  23248  fbflim  23487  alexsubALTlem3  23560  metss  24024  iscmet3lem2  24816  ovoliunlem3  25028  mbfposr  25176  i1fmulclem  25227  itg10a  25235  iblss  25329  dvlip  25517  plyeq0lem  25731  mtest  25923  itgulm  25927  dchrisumlem3  27001  rpvmasum2  27022  pntlem3  27119  nosupbday  27215  noinfbday  27230  hlpasch  28045  f1otrg  28160  lfgrwlkprop  28982  wlkiswwlks1  29159  frgrnbnb  29584  frgr2wwlkeqm  29622  unidifsnne  31811  hashxpe  32057  ccatf1  32153  signstfvneq0  33652  bnj605  33987  matunitlindflem1  36570  matunitlindflem2  36571  poimirlem26  36600  mblfinlem2  36612  ssfiunibd  44098  xralrple2  44143  infleinf  44161  infxrpnf  44235  fprodcn  44395  limsupub  44499  limsuppnflem  44505  limsupmnflem  44515  cnrefiisplem  44624  climxlim2lem  44640  icccncfext  44682  cncficcgt0  44683  cncfioobd  44692  dvbdfbdioolem2  44724  itgspltprt  44774  stoweidlem34  44829  stoweidlem49  44844  stoweidlem57  44852  fourierdlem34  44936  fourierdlem39  44941  fourierdlem50  44951  fourierdlem51  44952  fourierdlem64  44965  fourierdlem73  44974  fourierdlem77  44978  fourierdlem81  44982  fourierdlem94  44995  fourierdlem97  44998  fourierdlem103  45004  fourierdlem104  45005  fourierdlem113  45014  fourier2  45022  etransclem24  45053  intsal  45125  sge0pr  45189  sge0iunmptlemfi  45208  sge0seq  45241  sge0reuz  45242  nnfoctbdjlem  45250  meadjiunlem  45260  ismeannd  45262  carageniuncllem2  45317  isomennd  45326  hoicvr  45343  hspmbllem2  45422  iunhoiioolem  45470  iunhoiioo  45471  vonioo  45477  vonicc  45480  preimageiingt  45515  preimaleiinlt  45516  smfaddlem1  45558  smfaddlem2  45559  smflimlem4  45569  smfrec  45584  smfinflem  45612  sprsymrelf1lem  46238  lighneallem3  46354  isomgreqve  46572  subrngint  46818  1arymaptfo  47407