Theorem 3adant1 1128

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Hypothesis

Ref	Expression
3adant.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
3adant1	⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem 3adant1

Step	Hyp	Ref	Expression
1		3adant.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantll 710	. 2 ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)
3	2	3impa 1108	1 ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  3ad2ant2  1132  3ad2ant3  1133  3simpc  1148  eupickb  2629  spc3egv  3592  sbciegft  3814  reuhyp  5417  predtrss  6322  onunel  6468  funopg  6581  funprg  6601  funtpg  6602  funcnvtp  6610  unima  6965  fvun1  6981  fnreseql  7048  xpprsng  7139  ftpg  7155  f13dfv  7274  f1ofvswap  7306  mpoeq3ia  7489  ordunel  7817  fex2  7926  funexw  7940  poxp  8116  poxp2  8131  poxp3  8138  poseq  8146  suppval1  8154  wfr3g  8309  smores3  8355  oaord  8549  oacan  8550  oaword  8551  omord  8570  omcan  8571  omwordri  8574  odi  8581  omass  8582  oeord  8590  oecan  8591  oewordri  8594  oeordsuc  8596  nnaord  8621  nnaordr  8622  nndi  8625  nnmass  8626  nnaword  8629  nnmord  8634  nnmwordri  8638  naddelim  8687  naddel1  8688  naddel2  8689  naddss1  8690  naddss2  8691  naddasslem2  8696  nadd32  8698  erov  8810  ecopovtrn  8816  ixpf  8916  f1oen4g  8962  f1dom4g  8963  mapxpen  9145  dif1enlemOLD  9159  ssfi  9175  sbthfilem  9203  sbthfi  9204  onomeneq  9230  fimax2g  9291  unbnn  9301  funisfsupp  9369  inelfi  9415  elfiun  9427  sup0  9463  suppr  9468  infpr  9500  ttrclss  9717  frr3g  9753  r111  9772  dif1card  10007  ackbij1lem16  10232  cff1  10255  cfflb  10256  cfsmolem  10267  fin23lem34  10343  hsmexlem2  10424  axcc3  10435  domtriomlem  10439  axdc3lem4  10450  axdc4lem  10452  axcclem  10454  konigthlem  10565  gchdomtri  10626  tskpr  10767  tskop  10768  tskuni  10780  tskun  10783  gruop  10802  gruun  10803  grudomon  10814  adderpqlem  10951  mulerpqlem  10952  addassnq  10955  mulassnq  10956  distrnq  10958  ltsonq  10966  ltanq  10968  ltmnq  10969  genpass  11006  distrlem1pr  11022  distrlem4pr  11023  ltsopr  11029  adddir  11209  axlttrn  11290  ltletr  11310  letr  11312  mul32  11384  mul31  11385  add32  11436  subsub23  11469  addsubass  11474  subcan2  11489  subsub2  11492  nppcan2  11495  sub32  11498  nnncan  11499  nnncan2  11501  pnpcan2  11504  subdi  11651  subdir  11652  receu  11863  mulcan1g  11871  mulcan2g  11872  divmul3  11881  divrec  11892  divrec2  11893  divsubdir  11912  subdivcomb2  11914  divdiv1  11929  redivcl  11937  div2neg  11941  ltmul2  12069  lemul1  12070  lemul2  12071  lemul2a  12073  lediv1  12083  gt0div  12084  ge0div  12085  mulsuble0b  12090  ltdivmul  12093  ledivmul  12094  ltdivmul2  12095  ledivmul2  12097  lemuldiv  12098  ltdiv23  12109  lediv23  12110  ledivp1i  12143  ltdivp1i  12144  uzind2  12659  nn0ind  12661  fnn0ind  12665  uz3m2nn  12879  xrltletr  13140  xrletr  13141  xrre2  13153  xrltmin  13165  xrlemin  13167  xleadd2a  13237  xleadd1  13238  xltadd2  13240  xmulasslem3  13269  xmulass  13270  xltmul2  13276  ixxdisj  13343  iooneg  13452  iccneg  13453  icoshft  13454  icoshftf1o  13455  icodisj  13457  snunioo  13459  fzen  13522  ssfzunsnext  13550  fzrev3  13571  2ffzeq  13626  fzoaddel2  13692  elfzodifsumelfzo  13702  ssfzoulel  13730  ssfzo12bi  13731  fzoshftral  13753  adddivflid  13787  flltdivnn0lt  13802  ltdifltdiv  13803  fldiv4p1lem1div2  13804  modcyc  13875  modcyc2  13876  modaddabs  13878  modsubmodmod  13899  modaddmodup  13903  modaddmulmod  13907  moddi  13908  modsubdir  13909  expdiv  14083  digit2  14203  nfile  14323  hashdifpr  14379  hashgt23el  14388  hashreshashfun  14403  fi1uzind  14462  ccatval1  14531  ccatass  14542  swrdval  14597  swrdnd  14608  swrd0  14612  swrdfv2  14615  pfxsuff1eqwrdeq  14653  swrdswrdlem  14658  pfxccatin12lem2a  14681  pfxccatin12lem1  14682  repswccat  14740  cshwidxmod  14757  cshwidxmodr  14758  cshf1  14764  repswcshw  14766  2cshw  14767  2cshwcom  14770  2cshwcshw  14780  cshwcsh2id  14783  ccatco  14790  2swrd2eqwrdeq  14908  wwlktovf  14911  brcnvtrclfv  14954  shftval2  15026  mulre  15072  absdiv  15246  absdiflt  15268  absdifle  15269  abs3dif  15282  cau3  15306  ello12r  15465  elo12r  15476  modfsummods  15743  geoisum1c  15830  rpnnen2lem4  16164  rpnnen2lem7  16167  dvdsmulc  16231  dvdsmulcr  16233  dvdsmultr1  16243  dvdsmultr2  16245  dvdssub2  16248  oexpneg  16292  divalgb  16351  ndvdsadd  16357  sadass  16416  modgcd  16478  dvdsgcd  16490  dvdsgcdb  16491  gcdass  16493  mulgcd  16494  absmulgcd  16495  rpmulgcd  16502  nn0seqcvgd  16511  algcvga  16520  lcmdvdsb  16554  lcmass  16555  lcmfunsnlem1  16578  lcmfunsnlem2lem1  16579  lcmfunsnlem2lem2  16580  coprmdvds  16594  coprmdvds2  16595  rpmul  16600  cncongr1  16608  cncongr2  16609  qnumdenbi  16684  modprm0  16742  coprimeprodsq  16745  pythagtriplem4  16756  pythagtriplem8  16760  pythagtriplem9  16761  pythagtriplem12  16763  pythagtriplem14  16765  pythagtriplem16  16767  pcpremul  16780  pcgcd  16815  vdwapval  16910  vdwapun  16911  prmgaplem3  16990  prmgaplem4  16991  prmgaplem7  16994  prmgapprmolem  16998  mreiincl  17544  mreincl  17547  mremre  17552  mrcss  17564  catcisolem  18064  pleval2  18294  pospo  18302  latlem  18394  latjcom  18404  latmcom  18420  lubss  18470  lubun  18472  clatglbss  18476  ipole  18491  ipolt  18492  pslem  18529  dirtr  18559  gsumsgrpccat  18757  gsumws2  18759  frmdmnd  18776  symggrplem  18801  isgrpi  18881  grpsubrcan  18940  grpinvsub  18941  grpsubeq0  18945  grpsubadd0sub  18946  grpnpcan  18951  qussub  19106  ghmsub  19138  symgpssefmnd  19304  symggrp  19309  symgextsymg  19333  gsmsymgreqlem2  19340  symgfixfolem1  19347  pmtrprfv3  19363  symggen  19379  lsmass  19578  efgsrel  19643  cntzcmn  19749  dvrcl  20295  unitdvcl  20296  dvrcan1  20300  subrngmre  20450  subrgmre  20487  abvsubtri  20586  abvtrivd  20591  lmodvsubval2  20671  rmodislmodlem  20683  rmodislmod  20684  rmodislmodOLD  20685  lss0cl  20701  lssintcl  20719  lssincl  20720  reslmhm2  20808  lspvadd  20851  lspsntrim  20853  islbs3  20913  rnglidlmmgm  21034  rrgeq0  21106  cncrng  21166  xrsmcmn  21168  cndrng  21174  cnsrng  21179  xrs1mnd  21183  absabv  21202  psgnco  21355  zrhpsgninv  21357  zrhpsgnevpm  21363  zrhpsgnodpm  21364  zrhpsgnelbas  21366  zrhcopsgnelbas  21367  uvcresum  21567  lindfmm  21601  lindsmm  21602  evlsval2  21869  mamudm  22110  mamufacex  22111  matsubgcell  22156  matsc  22172  scmatscmide  22229  scmatrhmcl  22250  1marepvsma1  22305  m1detdiag  22319  mdetralt  22330  m2detleiblem7  22349  gsummatr01lem3  22379  gsummatr01  22381  smadiadetlem0  22383  decpmate  22488  decpmatcl  22489  pm2mpcl  22519  pm2mpghmlem2  22534  chfacfscmul0  22580  chfacfscmulgsum  22582  chfacfpmmul0  22584  chfacfpmmulgsum  22586  unopn  22625  clsss  22778  cldmre  22802  toponmre  22817  opnssneib  22839  restabs  22889  restcls  22905  restntr  22906  hausnei2  23077  cmpsublem  23123  bwth  23134  hausmapdom  23224  ptpjcn  23335  upxp  23347  ptrescn  23363  xkopjcn  23380  fbssfi  23561  snfil  23588  ufprim  23633  rnelfm  23677  flimrest  23707  fclsrest  23748  tmdgsum  23819  blpnfctr  24162  mscl  24187  xmscl  24188  xmsge0  24189  xmseq0  24190  restmetu  24299  ngpds  24333  tngngp3  24393  unitnmn0  24405  xrsxmet  24545  metds0  24586  mpomulcn  24605  cncfmptc  24652  isclmp  24844  cnlmod  24887  ncvsi  24899  cphsqrtcl  24932  cfil3i  25017  cfilres  25044  cmssmscld  25098  cmmbl  25283  voliunlem2  25300  itg2ub  25483  itgrecl  25547  tdeglem3OLD  25811  r1pid  25912  eflogeq  26346  cxpadd  26423  cxpcom  26483  logbchbase  26512  relogbreexp  26516  relogbzexp  26517  relogbmulexp  26519  logbleb  26524  logblt  26525  lawcos  26557  pythag  26558  asinsinb  26638  acoscosb  26639  atantanb  26665  amgmlem  26730  lgsneg  27060  lgsne0  27074  lgsmodeq  27081  lgsmulsqcoprm  27082  gausslemma2dlem1a  27104  2sqreulem2  27191  sltres  27401  noetainflem1  27476  sltletr  27495  sletr  27497  nocvxmin  27516  madebdaylemold  27629  lrrecpo  27663  sltadd2im  27708  sleadd1im  27709  sleadd2im  27710  sleadd1  27711  sleadd2  27712  sltadd1  27714  addscan2  27715  addscan1  27716  subadds  27777  sltsub1  27782  divscl  27908  brbtwn2  28430  colinearalg  28435  eleesubd  28437  axcgrrflx  28439  axcgrtr  28440  axsegcon  28452  ax5seglem1  28453  ax5seglem2  28454  ax5seglem4  28457  axbtwnid  28464  axlowdimlem14  28480  axlowdim  28486  axcontlem5  28493  axcontlem7  28495  nb3grprlem2  28905  cplgr3v  28959  cusgrsizeindslem  28975  sizusglecusglem2  28986  umgr2v2e  29049  cusgrrusgr  29105  iswlk  29134  edginwlk  29159  uspgr2wlkeq  29170  uspgr2wlkeq2  29171  uspgr2wlkeqi  29172  wlkonprop  29182  wlkon2n0  29190  pthdadjvtx  29254  upgr2pthnlp  29256  spthonepeq  29276  pthdlem2lem  29291  crctcshwlkn0lem3  29333  crctcshwlkn0lem5  29335  wlkiswwlks2lem4  29393  wlkiswwlks2lem6  29395  wlklnwwlkln2lem  29403  wwlksnred  29413  wwlksnextbi  29415  wwlksnextwrd  29418  2pthdlem1  29451  2wlkdlem10  29456  umgr2adedgwlkonALT  29468  elwwlks2s3  29472  elwwlks2ons3im  29475  s3wwlks2on  29477  2wspdisj  29483  2wspiundisj  29484  clwwlkgt0  29506  clwlkclwwlklem2a4  29517  clwlkclwwlklem2a  29518  clwlkclwwlk  29522  clwlkclwwlk2  29523  clwlkclwwlkfo  29529  clwwisshclwwslemlem  29533  erclwwlktr  29542  clwwlkf  29567  wwlksubclwwlk  29578  erclwwlkntr  29591  clwwlknon  29610  frcond1  29786  frgr3v  29795  3vfriswmgr  29798  frgrwopreglem4a  29830  frrusgrord0lem  29859  clwwnonrepclwwnon  29865  extwwlkfab  29872  numclwwlk1lem2f1  29877  numclwwlk1lem2fo  29878  clwlknon2num  29888  numclwwlk2lem1  29896  numclwlk2lem2f  29897  numclwlk2lem2f1o  29899  numclwwlk2  29901  frgrreggt1  29913  friendshipgt3  29918  imsmetlem  30210  nmoxr  30286  nmoolb  30291  blometi  30323  phpar2  30343  phpar  30344  ipasslem5  30355  hvadd32  30554  hvaddsub12  30558  hvaddsubass  30561  hvsubass  30564  hvsub32  30565  hvsubdistr1  30569  hvsubdistr2  30570  hvmulcan  30592  hvmulcan2  30593  hvsubcan  30594  his5  30606  his2sub  30612  hhssabloilem  30781  hhssnv  30784  shlej2  30881  pjoi0  31237  hodcl  31267  hoadd32  31303  hosubdi  31328  hosubsub2  31332  hoaddsubass  31335  hosubsub4  31338  nmoplb  31427  unop  31435  hmop  31442  nmfnlb  31444  lnopmul  31487  kbass1  31636  kbass2  31637  leopmul2i  31655  leoptr  31657  cvntr  31812  mdslmd4i  31853  mdexchi  31855  atcv1  31900  sumdmdii  31935  fcoinvbr  32103  fpwrelmapffs  32226  xreceu  32355  isinftm  32597  unitdivcld  33179  esummulc1  33377  hasheuni  33381  unelsiga  33430  inelpisys  33450  carsgsigalem  33612  signswmnd  33866  bnj545  34204  bnj594  34221  bnj1311  34333  fineqvac  34395  hashf1dmcdm  34403  usgrgt2cycl  34419  subgrwlk  34421  acycgr1v  34438  cvmsf1o  34561  cvmscld  34562  satefvfmla1  34714  elnanelprv  34718  lediv2aALT  34960  gcd32  35023  fununiq  35044  dfrdg4  35227  brcolinear  35335  colinearex  35336  gg-cncrng  35486  nn0prpwlem  35510  clsun  35516  fnemeet1  35554  fnemeet2  35555  fnejoin1  35556  fnejoin2  35557  eltail  35562  rdgeqoa  36554  nlpineqsn  36592  curf  36769  lindsadd  36784  poimirlem28  36819  cnambfre  36839  ftc1anclem4  36867  cocanfo  36890  f1ocan1fv  36897  metf1o  36926  ismtybnd  36978  ghomco  37062  isdrngo2  37129  inidl  37201  igenmin  37235  brxrn  37547  brredunds  37799  cmtvalN  38384  cvrval  38442  pmapmeet  38947  paddval  38972  paddssat  38988  elpcliN  39067  pclssN  39068  pclunN  39072  paddunN  39101  poldmj1N  39102  tendoplcl2  39952  tendoplcl  39955  dihmeet  40517  lcmineqlem1  41200  factwoffsmonot  41329  expgcd  41527  zexpgcd  41529  reltsub1  41561  reltsubadd2  41562  resubsub4  41564  reppncan  41568  resubdi  41571  readdcan2  41587  subresre  41605  mapco2g  41754  mzpcompact2lem  41791  eqrabdioph  41817  lerabdioph  41845  eluzrabdioph  41846  ltrabdioph  41848  nerabdioph  41849  dvdsrabdioph  41850  reglogcl  41930  rmxyadd  41962  rmyabs  41999  congadd  42007  congabseq  42015  rmydioph  42055  mendring  42236  mendlmod  42237  iocinico  42263  omge1  42349  relexp0a  42769  relexpaddss  42771  brcoffn  43083  ismnushort  43362  dvconstbi  43395  uzwo4  44041  ssin0  44043  ssinc  44077  ssdec  44078  fvmpt2bd  44167  disjf1o  44188  ssnnf1octb  44191  sub31  44298  fperiodmullem  44311  ssfiunibd  44317  infxr  44375  fmul01  44594  islptre  44633  lptre2pt  44654  limcleqr  44658  limclner  44665  limsuppnflem  44724  limsupvaluz2  44752  supcnvlimsup  44754  xlimmnfvlem2  44847  xlimmnfv  44848  xlimpnfvlem2  44851  xlimpnfv  44852  climxlim2lem  44859  coskpi2  44880  cosknegpi  44883  dvnmptdivc  44952  dvdsn1add  44953  dvnmptconst  44955  dvmptfprod  44959  dvnprodlem1  44960  dvnprodlem2  44961  ovolsplit  45002  stoweidlem60  45074  stowei  45078  dirkeritg  45116  fourierdlem70  45190  fourierdlem71  45191  fourierdlem103  45223  fourierdlem104  45224  fouriersw  45245  rrxtopnfi  45301  saluncl  45331  salexct  45348  sge0ltfirp  45414  sge0iunmpt  45432  meadjiunlem  45479  meaiuninc3v  45498  carageniuncllem1  45535  caratheodorylem1  45540  ovncvrrp  45578  ovnsubaddlem1  45584  hspmbllem2  45641  ovolval5lem3  45668  smfpimbor1lem1  45812  smfsuplem1  45825  smflimsuplem4  45837  sigarls  45871  cnambpcma  46300  elfzelfzlble  46327  fzoopth  46333  m1mod0mod1  46335  fsumsplitsndif  46339  fundcmpsurinjALT  46378  iccpartiltu  46388  prproropf1olem2  46470  fmtno4prmfac  46538  2pwp1prmfmtno  46556  lighneallem4b  46575  mogoldbblem  46686  gbegt5  46727  sbgoldbm  46750  nnsum3primesle9  46760  nnsum4primesodd  46762  nnsum4primesoddALTV  46763  evengpoap3  46765  nnsum4primesevenALTV  46767  isomgrtr  46805  strisomgrop  46806  isupwlk  46812  lidldomnnring  46916  2zrngacmnd  46928  rhmsubclem2  47073  rhmsubcALTVlem2  47091  fprmappr  47109  zlmodzxzscm  47121  gsumlsscl  47147  lincvalsng  47184  lincvalpr  47186  lincdifsn  47192  linc1  47193  lincellss  47194  difmodm1lt  47295  fdivmpt  47313  digexp  47380  2arymaptfo  47427  line  47505  rrxline  47507  itsclc0xyqsolr  47542  iscnrm3r  47668  amgmwlem  47936