Theorem 3adant1 1129

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 711	. 2 ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)
3	2	3impa 1109	1 ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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  df-3an 1088

This theorem is referenced by:  3ad2ant2  1133  3ad2ant3  1134  3simpc  1149  eupickb  2638  spc3egv  3543  sbciegft  3755  reuhyp  5344  predtrss  6229  funopg  6475  funprg  6495  funtpg  6496  funcnvtp  6504  unima  6852  fvun1  6868  fnreseql  6934  xpprsng  7021  ftpg  7037  f13dfv  7155  f1ofvswap  7187  mpoeq3ia  7362  ordunel  7683  fex2  7789  funexw  7803  poxp  7978  suppval1  7992  wfr3g  8147  smores3  8193  oaord  8387  oacan  8388  oaword  8389  omord  8408  omcan  8409  omwordri  8412  odi  8419  omass  8420  oeord  8428  oecan  8429  oewordri  8432  oeordsuc  8434  nnaord  8459  nnaordr  8460  nndi  8463  nnmass  8464  nnaword  8467  nnmord  8472  nnmwordri  8476  erov  8612  ecopovtrn  8618  ixpf  8717  mapxpen  8939  dif1enlem  8952  ssfi  8965  sbthfilem  8993  sbthfi  8994  onomeneq  9020  fimax2g  9069  unbnn  9079  funisfsupp  9142  inelfi  9186  elfiun  9198  sup0  9234  suppr  9239  infpr  9271  ttrclss  9487  frr3g  9523  r111  9542  dif1card  9775  ackbij1lem16  10000  cff1  10023  cfflb  10024  cfsmolem  10035  fin23lem34  10111  hsmexlem2  10192  axcc3  10203  domtriomlem  10207  axdc3lem4  10218  axdc4lem  10220  axcclem  10222  konigthlem  10333  gchdomtri  10394  tskpr  10535  tskop  10536  tskuni  10548  tskun  10551  gruop  10570  gruun  10571  grudomon  10582  adderpqlem  10719  mulerpqlem  10720  addassnq  10723  mulassnq  10724  distrnq  10726  ltsonq  10734  ltanq  10736  ltmnq  10737  genpass  10774  distrlem1pr  10790  distrlem4pr  10791  ltsopr  10797  adddir  10975  axlttrn  11056  ltletr  11076  letr  11078  mul32  11150  mul31  11151  add32  11202  subsub23  11235  addsubass  11240  subcan2  11255  subsub2  11258  nppcan2  11261  sub32  11264  nnncan  11265  nnncan2  11267  pnpcan2  11270  subdi  11417  subdir  11418  receu  11629  mulcan1g  11637  mulcan2g  11638  divmul3  11647  divrec  11658  divrec2  11659  divsubdir  11678  subdivcomb2  11680  divdiv1  11695  redivcl  11703  div2neg  11707  ltmul2  11835  lemul1  11836  lemul2  11837  lemul2a  11839  lediv1  11849  gt0div  11850  ge0div  11851  mulsuble0b  11856  ltdivmul  11859  ledivmul  11860  ltdivmul2  11861  ledivmul2  11863  lemuldiv  11864  ltdiv23  11875  lediv23  11876  ledivp1i  11909  ltdivp1i  11910  uzind2  12422  nn0ind  12424  fnn0ind  12428  uz3m2nn  12640  xrltletr  12900  xrletr  12901  xrre2  12913  xrltmin  12925  xrlemin  12927  xleadd2a  12997  xleadd1  12998  xltadd2  13000  xmulasslem3  13029  xmulass  13030  xltmul2  13036  ixxdisj  13103  iooneg  13212  iccneg  13213  icoshft  13214  icoshftf1o  13215  icodisj  13217  snunioo  13219  fzen  13282  ssfzunsnext  13310  fzrev3  13331  2ffzeq  13386  fzoaddel2  13452  elfzodifsumelfzo  13462  ssfzoulel  13490  ssfzo12bi  13491  fzoshftral  13513  adddivflid  13547  flltdivnn0lt  13562  ltdifltdiv  13563  fldiv4p1lem1div2  13564  modcyc  13635  modcyc2  13636  modaddabs  13638  modsubmodmod  13659  modaddmodup  13663  modaddmulmod  13667  moddi  13668  modsubdir  13669  expdiv  13843  digit2  13960  nfile  14083  hashdifpr  14139  hashgt23el  14148  hashreshashfun  14163  fi1uzind  14220  ccatval1  14290  ccatass  14302  swrdval  14365  swrdnd  14376  swrd0  14380  swrdfv2  14383  pfxsuff1eqwrdeq  14421  swrdswrdlem  14426  pfxccatin12lem2a  14449  pfxccatin12lem1  14450  repswccat  14508  cshwidxmod  14525  cshwidxmodr  14526  cshf1  14532  repswcshw  14534  2cshw  14535  2cshwcom  14538  2cshwcshw  14547  cshwcsh2id  14550  ccatco  14557  2swrd2eqwrdeq  14675  wwlktovf  14680  brcnvtrclfv  14723  shftval2  14795  mulre  14841  absdiv  15016  absdiflt  15038  absdifle  15039  abs3dif  15052  cau3  15076  ello12r  15235  elo12r  15246  modfsummods  15514  geoisum1c  15601  rpnnen2lem4  15935  rpnnen2lem7  15938  dvdsmulc  16002  dvdsmulcr  16004  dvdsmultr1  16014  dvdsmultr2  16016  dvdssub2  16019  oexpneg  16063  divalgb  16122  ndvdsadd  16128  sadass  16187  modgcd  16249  dvdsgcd  16261  dvdsgcdb  16262  gcdass  16264  mulgcd  16265  absmulgcd  16266  rpmulgcd  16275  nn0seqcvgd  16284  algcvga  16293  lcmdvdsb  16327  lcmass  16328  lcmfunsnlem1  16351  lcmfunsnlem2lem1  16352  lcmfunsnlem2lem2  16353  coprmdvds  16367  coprmdvds2  16368  rpmul  16373  cncongr1  16381  cncongr2  16382  qnumdenbi  16457  modprm0  16515  coprimeprodsq  16518  pythagtriplem4  16529  pythagtriplem8  16533  pythagtriplem9  16534  pythagtriplem12  16536  pythagtriplem14  16538  pythagtriplem16  16540  pcpremul  16553  pcgcd  16588  vdwapval  16683  vdwapun  16684  prmgaplem3  16763  prmgaplem4  16764  prmgaplem7  16767  prmgapprmolem  16771  mreiincl  17314  mreincl  17317  mremre  17322  mrcss  17334  catcisolem  17834  pleval2  18064  pospo  18072  latlem  18164  latjcom  18174  latmcom  18190  lubss  18240  lubun  18242  clatglbss  18246  ipole  18261  ipolt  18262  pslem  18299  dirtr  18329  gsumsgrpccat  18487  gsumws2  18490  frmdmnd  18507  symggrplem  18532  isgrpi  18611  grpsubrcan  18665  grpinvsub  18666  grpsubeq0  18670  grpsubadd0sub  18671  grpnpcan  18676  qussub  18825  ghmsub  18851  symgpssefmnd  19012  symggrp  19017  symgextsymg  19041  gsmsymgreqlem2  19048  symgfixfolem1  19055  pmtrprfv3  19071  symggen  19087  lsmass  19284  efgsrel  19349  cntzcmn  19450  dvrcl  19937  unitdvcl  19938  dvrcan1  19942  subrgmre  20057  abvsubtri  20104  abvtrivd  20109  lmodvsubval2  20187  rmodislmodlem  20199  rmodislmod  20200  rmodislmodOLD  20201  lss0cl  20217  lssintcl  20235  lssincl  20236  reslmhm2  20324  lspvadd  20367  lspsntrim  20369  islbs3  20426  rrgeq0  20570  cncrng  20628  xrsmcmn  20630  cndrng  20636  cnsrng  20641  xrs1mnd  20645  absabv  20664  psgnco  20797  zrhpsgninv  20799  zrhpsgnevpm  20805  zrhpsgnodpm  20806  zrhpsgnelbas  20808  zrhcopsgnelbas  20809  uvcresum  21009  lindfmm  21043  lindsmm  21044  evlsval2  21306  mamudm  21546  mamufacex  21547  matsubgcell  21592  matsc  21608  scmatscmide  21665  scmatrhmcl  21686  1marepvsma1  21741  m1detdiag  21755  mdetralt  21766  m2detleiblem7  21785  gsummatr01lem3  21815  gsummatr01  21817  smadiadetlem0  21819  decpmate  21924  decpmatcl  21925  pm2mpcl  21955  pm2mpghmlem2  21970  chfacfscmul0  22016  chfacfscmulgsum  22018  chfacfpmmul0  22020  chfacfpmmulgsum  22022  unopn  22061  clsss  22214  cldmre  22238  toponmre  22253  opnssneib  22275  restabs  22325  restcls  22341  restntr  22342  hausnei2  22513  cmpsublem  22559  bwth  22570  hausmapdom  22660  ptpjcn  22771  upxp  22783  ptrescn  22799  xkopjcn  22816  fbssfi  22997  snfil  23024  ufprim  23069  rnelfm  23113  flimrest  23143  fclsrest  23184  tmdgsum  23255  blpnfctr  23598  mscl  23623  xmscl  23624  xmsge0  23625  xmseq0  23626  restmetu  23735  ngpds  23769  tngngp3  23829  unitnmn0  23841  xrsxmet  23981  metds0  24022  cncfmptc  24084  isclmp  24269  cnlmod  24312  ncvsi  24324  cphsqrtcl  24357  cfil3i  24442  cfilres  24469  cmssmscld  24523  cmmbl  24707  voliunlem2  24724  itg2ub  24907  itgrecl  24971  tdeglem3OLD  25232  r1pid  25333  eflogeq  25766  cxpadd  25843  cxpcom  25901  logbchbase  25930  relogbreexp  25934  relogbzexp  25935  relogbmulexp  25937  logbleb  25942  logblt  25943  lawcos  25975  pythag  25976  asinsinb  26056  acoscosb  26057  atantanb  26083  amgmlem  26148  lgsneg  26478  lgsne0  26492  lgsmodeq  26499  lgsmulsqcoprm  26500  gausslemma2dlem1a  26522  2sqreulem2  26609  brbtwn2  27282  colinearalg  27287  eleesubd  27289  axcgrrflx  27291  axcgrtr  27292  axsegcon  27304  ax5seglem1  27305  ax5seglem2  27306  ax5seglem4  27309  axbtwnid  27316  axlowdimlem14  27332  axlowdim  27338  axcontlem5  27345  axcontlem7  27347  nb3grprlem2  27757  cplgr3v  27811  cusgrsizeindslem  27827  sizusglecusglem2  27838  umgr2v2e  27901  cusgrrusgr  27957  iswlk  27986  edginwlk  28011  uspgr2wlkeq  28022  uspgr2wlkeq2  28023  uspgr2wlkeqi  28024  wlkonprop  28035  wlkon2n0  28043  pthdadjvtx  28107  upgr2pthnlp  28109  spthonepeq  28129  pthdlem2lem  28144  crctcshwlkn0lem3  28186  crctcshwlkn0lem5  28188  wlkiswwlks2lem4  28246  wlkiswwlks2lem6  28248  wlklnwwlkln2lem  28256  wwlksnred  28266  wwlksnextbi  28268  wwlksnextwrd  28271  2pthdlem1  28304  2wlkdlem10  28309  umgr2adedgwlkonALT  28321  elwwlks2s3  28325  elwwlks2ons3im  28328  s3wwlks2on  28330  2wspdisj  28336  2wspiundisj  28337  clwwlkgt0  28359  clwlkclwwlklem2a4  28370  clwlkclwwlklem2a  28371  clwlkclwwlk  28375  clwlkclwwlk2  28376  clwlkclwwlkfo  28382  clwwisshclwwslemlem  28386  erclwwlktr  28395  clwwlkf  28420  wwlksubclwwlk  28431  erclwwlkntr  28444  clwwlknon  28463  frcond1  28639  frgr3v  28648  3vfriswmgr  28651  frgrwopreglem4a  28683  frrusgrord0lem  28712  clwwnonrepclwwnon  28718  extwwlkfab  28725  numclwwlk1lem2f1  28730  numclwwlk1lem2fo  28731  clwlknon2num  28741  numclwwlk2lem1  28749  numclwlk2lem2f  28750  numclwlk2lem2f1o  28752  numclwwlk2  28754  frgrreggt1  28766  friendshipgt3  28771  imsmetlem  29061  nmoxr  29137  nmoolb  29142  blometi  29174  phpar2  29194  phpar  29195  ipasslem5  29206  hvadd32  29405  hvaddsub12  29409  hvaddsubass  29412  hvsubass  29415  hvsub32  29416  hvsubdistr1  29420  hvsubdistr2  29421  hvmulcan  29443  hvmulcan2  29444  hvsubcan  29445  his5  29457  his2sub  29463  hhssabloilem  29632  hhssnv  29635  shlej2  29732  pjoi0  30088  hodcl  30118  hoadd32  30154  hosubdi  30179  hosubsub2  30183  hoaddsubass  30186  hosubsub4  30189  nmoplb  30278  unop  30286  hmop  30293  nmfnlb  30295  lnopmul  30338  kbass1  30487  kbass2  30488  leopmul2i  30506  leoptr  30508  cvntr  30663  mdslmd4i  30704  mdexchi  30706  atcv1  30751  sumdmdii  30786  fcoinvbr  30956  fpwrelmapffs  31078  xreceu  31205  isinftm  31444  unitdivcld  31860  esummulc1  32058  hasheuni  32062  unelsiga  32111  inelpisys  32131  carsgsigalem  32291  signswmnd  32545  bnj545  32884  bnj594  32901  bnj1311  33013  fineqvac  33075  hashf1dmcdm  33085  usgrgt2cycl  33101  subgrwlk  33103  acycgr1v  33120  cvmsf1o  33243  cvmscld  33244  satefvfmla1  33396  elnanelprv  33400  lediv2aALT  33644  onunel  33698  gcd32  33724  fununiq  33752  poxp2  33799  poxp3  33805  poseq  33811  naddelim  33847  naddel1  33848  naddel2  33849  naddss1  33850  naddss2  33851  sltres  33874  noetainflem1  33949  sltletr  33968  sletr  33970  nocvxmin  33982  madebdaylemold  34087  lrrecpo  34107  dfrdg4  34262  brcolinear  34370  colinearex  34371  nn0prpwlem  34520  clsun  34526  fnemeet1  34564  fnemeet2  34565  fnejoin1  34566  fnejoin2  34567  eltail  34572  rdgeqoa  35550  nlpineqsn  35588  curf  35764  lindsadd  35779  poimirlem28  35814  cnambfre  35834  ftc1anclem4  35862  cocanfo  35885  f1ocan1fv  35893  metf1o  35922  ismtybnd  35974  ghomco  36058  isdrngo2  36125  inidl  36197  igenmin  36231  brxrn  36511  brredunds  36746  cmtvalN  37232  cvrval  37290  pmapmeet  37794  paddval  37819  paddssat  37835  elpcliN  37914  pclssN  37915  pclunN  37919  paddunN  37948  poldmj1N  37949  tendoplcl2  38799  tendoplcl  38802  dihmeet  39364  lcmineqlem1  40044  factwoffsmonot  40170  expgcd  40341  zexpgcd  40343  reltsub1  40376  reltsubadd2  40377  resubsub4  40379  reppncan  40383  resubdi  40386  readdcan2  40402  subresre  40419  mapco2g  40543  mzpcompact2lem  40580  eqrabdioph  40606  lerabdioph  40634  eluzrabdioph  40635  ltrabdioph  40637  nerabdioph  40638  dvdsrabdioph  40639  reglogcl  40719  rmxyadd  40750  rmyabs  40787  congadd  40795  congabseq  40803  rmydioph  40843  mendring  41024  mendlmod  41025  iocinico  41050  relexp0a  41331  relexpaddss  41333  brcoffn  41647  ismnushort  41926  dvconstbi  41959  uzwo4  42608  ssin0  42610  ssinc  42644  ssdec  42645  fvmpt2bd  42713  disjf1o  42736  ssnnf1octb  42740  sub31  42836  fperiodmullem  42849  ssfiunibd  42855  infxr  42913  fmul01  43128  islptre  43167  lptre2pt  43188  limcleqr  43192  limclner  43199  limsuppnflem  43258  limsupvaluz2  43286  supcnvlimsup  43288  xlimmnfvlem2  43381  xlimmnfv  43382  xlimpnfvlem2  43385  xlimpnfv  43386  climxlim2lem  43393  coskpi2  43414  cosknegpi  43417  dvnmptdivc  43486  dvdsn1add  43487  dvnmptconst  43489  dvmptfprod  43493  dvnprodlem1  43494  dvnprodlem2  43495  ovolsplit  43536  stoweidlem60  43608  stowei  43612  dirkeritg  43650  fourierdlem70  43724  fourierdlem71  43725  fourierdlem103  43757  fourierdlem104  43758  fouriersw  43779  rrxtopnfi  43835  saluncl  43865  salexct  43880  sge0ltfirp  43945  sge0iunmpt  43963  meadjiunlem  44010  meaiuninc3v  44029  carageniuncllem1  44066  caratheodorylem1  44071  ovncvrrp  44109  ovnsubaddlem1  44115  hspmbllem2  44172  ovolval5lem3  44199  smfpimbor1lem1  44343  smfsuplem1  44355  smflimsuplem4  44367  sigarls  44384  cnambpcma  44797  elfzelfzlble  44824  fzoopth  44830  m1mod0mod1  44832  fsumsplitsndif  44836  fundcmpsurinjALT  44875  iccpartiltu  44885  prproropf1olem2  44967  fmtno4prmfac  45035  2pwp1prmfmtno  45053  lighneallem4b  45072  mogoldbblem  45183  gbegt5  45224  sbgoldbm  45247  nnsum3primesle9  45257  nnsum4primesodd  45259  nnsum4primesoddALTV  45260  evengpoap3  45262  nnsum4primesevenALTV  45264  isomgrtr  45302  strisomgrop  45303  isupwlk  45309  lidldomnnring  45499  2zrngacmnd  45511  rhmsubclem2  45656  rhmsubcALTVlem2  45674  fprmappr  45692  zlmodzxzscm  45704  gsumlsscl  45730  lincvalsng  45768  lincvalpr  45770  lincdifsn  45776  linc1  45777  lincellss  45778  difmodm1lt  45879  fdivmpt  45897  digexp  45964  2arymaptfo  46011  line  46089  rrxline  46091  itsclc0xyqsolr  46126  iscnrm3r  46253  amgmwlem  46517