Theorem 3adant1 1146

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3ad2ant2  1150  3ad2ant3  1151  3simpc  1166  eupickb  2669  spc3egv  3571  reuhyp  5389  predtrss  6321  onunel  6466  funopg  6568  funprg  6588  funtpg  6589  funcnvtp  6597  unima  6954  fvun1  6970  fnreseql  7041  xpprsng  7134  ftpg  7151  f1ounsn  7268  f13dfv  7270  f1ocoima  7299  f1ofvswap  7302  mpoeq3ia  7486  ordunel  7819  fex2  7929  funexw  7945  poxp  8120  poxp2  8135  poxp3  8142  poseq  8150  suppval1  8158  wfr3g  8312  smores3  8336  oaord  8528  oacan  8529  oaword  8530  omord  8549  omcan  8550  omwordri  8553  odi  8560  omass  8561  oeord  8570  oecan  8571  oewordri  8574  oeordsuc  8576  nnaord  8601  nnaordr  8602  nndi  8605  nnmass  8606  nnaword  8609  nnmord  8614  nnmwordri  8618  naddelim  8669  naddel1  8670  naddel2  8671  naddss1  8672  naddss2  8673  naddasslem2  8678  nadd32  8680  erov  8808  ecopovtrn  8814  ixpf  8914  f1oen4g  8957  f1dom4g  8958  mapxpen  9127  ssfi  9153  sbthfilem  9178  sbthfi  9179  onomeneq  9194  fimax2g  9242  unbnn  9252  funisfsupp  9323  inelfi  9374  elfiun  9386  sup0  9423  suppr  9428  infpr  9461  ttrclss  9685  frr3g  9724  r111  9743  dif1card  9990  ackbij1lem16  10213  cff1  10238  cfflb  10239  cfsmolem  10250  fin23lem34  10326  hsmexlem2  10407  axcc3  10418  domtriomlem  10422  axdc3lem4  10433  axdc4lem  10435  axcclem  10437  konigthlem  10549  gchdomtri  10610  tskpr  10751  tskop  10752  tskuni  10764  tskun  10767  gruop  10786  gruun  10787  grudomon  10798  adderpqlem  10935  mulerpqlem  10936  addassnq  10939  mulassnq  10940  distrnq  10942  ltsonq  10950  ltanq  10952  ltmnq  10953  genpass  10990  distrlem1pr  11006  distrlem4pr  11007  ltsopr  11013  adddir  11193  axlttrn  11278  ltletr  11298  letr  11300  mul32  11372  mul31  11373  add32  11425  subsub23  11458  addsubass  11463  subcan2  11479  subsub2  11482  nppcan2  11485  sub32  11488  nnncan  11489  nnncan2  11491  pnpcan2  11494  subdi  11643  subdir  11644  receu  11855  mulcan1g  11863  mulcan2g  11864  divmul3  11873  divrec  11884  divrec2  11885  div11  11896  divsubdir  11904  subdivcomb2  11907  divdiv1  11922  redivcl  11930  div2neg  11934  ltmul2  12062  lemul1  12063  lemul2  12064  lemul2a  12066  lediv1  12076  gt0div  12077  ge0div  12078  mulsuble0b  12083  ltdivmul  12086  ledivmul  12087  ltdivmul2  12088  ledivmul2  12090  lemuldiv  12091  ltdiv23  12102  lediv23  12103  ledivp1i  12136  ltdivp1i  12137  uzind2  12685  nn0ind  12687  fnn0ind  12691  uz3m2nn  12914  xrltletr  13178  xrletr  13179  xrre2  13192  xrltmin  13204  xrlemin  13206  xleadd2a  13276  xleadd1  13277  xltadd2  13279  xmulasslem3  13308  xmulass  13309  xltmul2  13315  ixxdisj  13383  iooneg  13494  iccneg  13495  icoshft  13496  icoshftf1o  13497  icodisj  13499  snunioo  13501  fzen  13565  ssfzunsnext  13593  fzrev3  13614  2ffzeq  13673  fzoaddel2  13745  elfzodifsumelfzo  13756  ssfzoulel  13785  ssfzo12bi  13786  fzoopth  13787  fzoshftral  13812  adddivflid  13847  flltdivnn0lt  13862  ltdifltdiv  13863  fldiv4p1lem1div2  13864  modcyc  13935  modcyc2  13936  modaddabs  13940  muladdmod  13944  modsubmodmod  13962  modaddmodup  13966  modaddmulmod  13970  moddi  13971  modsubdir  13972  expdiv  14145  digit2  14268  nfile  14391  hashdifpr  14448  hashgt23el  14457  hashreshashfun  14472  hashf1dmcdm  14477  hash3tpexb  14527  fi1uzind  14540  ccatval1  14610  ccatass  14622  swrdval  14677  swrdnd  14688  swrd0  14692  swrdfv2  14695  pfxsuff1eqwrdeq  14732  swrdswrdlem  14737  pfxccatin12lem2a  14760  pfxccatin12lem1  14761  repswccat  14819  cshwidxmod  14836  cshwidxmodr  14837  cshf1  14843  repswcshw  14845  2cshw  14846  2cshwcom  14849  2cshwcshw  14858  cshwcsh2id  14861  ccatco  14868  2swrd2eqwrdeq  14986  wwlktovf  14989  brcnvtrclfv  15036  shftval2  15108  mulre  15168  absdiv  15342  absdiflt  15365  absdifle  15366  abs3dif  15379  cau3  15403  ello12r  15564  elo12r  15575  modfsummods  15841  geoisum1c  15930  rpnnen2lem4  16269  rpnnen2lem7  16272  addmulmodb  16319  dvdsmulc  16337  dvdsmulcr  16339  dvdsmultr1  16350  dvdsmultr2  16352  dvdssub2  16355  oexpneg  16399  divalgb  16458  ndvdsadd  16464  sadass  16525  modgcd  16586  dvdsgcd  16598  dvdsgcdb  16599  gcdass  16601  mulgcd  16602  absmulgcd  16603  rpmulgcd  16611  expgcd  16617  zexpgcd  16619  nn0seqcvgd  16624  algcvga  16633  lcmdvdsb  16667  lcmass  16668  lcmfunsnlem1  16691  lcmfunsnlem2lem1  16692  lcmfunsnlem2lem2  16693  coprmdvds  16707  coprmdvds2  16708  rpmul  16713  cncongr1  16721  cncongr2  16722  qnumdenbi  16799  modprm0  16861  coprimeprodsq  16864  pythagtriplem4  16875  pythagtriplem8  16879  pythagtriplem9  16880  pythagtriplem12  16882  pythagtriplem14  16884  pythagtriplem16  16886  pcpremul  16899  pcgcd  16934  vdwapval  17029  vdwapun  17030  prmgaplem3  17109  prmgaplem4  17110  prmgaplem7  17113  prmgapprmolem  17117  mreiincl  17644  mreincl  17647  mremre  17652  mrcss  17668  catcisolem  18163  pleval2  18387  pospo  18395  latlem  18489  latjcom  18499  latmcom  18515  lubss  18565  lubun  18567  clatglbss  18571  ipole  18586  ipolt  18587  pslem  18624  dirtr  18654  gsumsgrpccat  18895  gsumws2  18897  frmdmnd  18914  symggrplem  18939  isgrpi  19022  grpsubrcan  19083  grpinvsub  19084  grpsubeq0  19088  grpsubadd0sub  19089  grpnpcan  19094  qussub  19258  ghmsub  19290  symgpssefmnd  19462  symggrp  19466  symgextsymg  19490  gsmsymgreqlem2  19497  symgfixfolem1  19504  pmtrprfv3  19520  symggen  19536  lsmass  19735  efgsrel  19800  cntzcmn  19906  dvrcl  20482  unitdvcl  20483  dvrcan1  20487  subrngmre  20643  subrgmre  20678  rhmsubclem2  20767  rrgeq0  20781  abvsubtri  20904  abvtrivd  20909  lmodvsubval2  21012  rmodislmodlem  21024  rmodislmod  21025  lss0cl  21042  lssintcl  21059  lssincl  21060  reslmhm2  21148  lspvadd  21191  lspsntrim  21193  islbs3  21253  unichnlidl  21336  rnglidlmmgm  21349  cncrng  21508  xrsmcmn  21510  cndrng  21516  cnsrng  21521  absabv  21539  xrs1mnd  21555  psgnco  21698  zrhpsgninv  21700  zrhpsgnevpm  21706  zrhpsgnodpm  21707  zrhpsgnelbas  21709  zrhcopsgnelbas  21710  uvcresum  21908  lindfmm  21942  lindsmm  21943  evlsval2  22203  mamudm  22517  mamufacex  22518  matsubgcell  22556  matsc  22572  scmatscmide  22629  scmatrhmcl  22650  1marepvsma1  22705  m1detdiag  22719  mdetralt  22730  m2detleiblem7  22749  gsummatr01lem3  22779  gsummatr01  22781  smadiadetlem0  22783  decpmate  22888  decpmatcl  22889  pm2mpcl  22919  pm2mpghmlem2  22934  chfacfscmul0  22980  chfacfscmulgsum  22982  chfacfpmmul0  22984  chfacfpmmulgsum  22986  unopn  23025  clsss  23176  cldmre  23200  toponmre  23215  opnssneib  23237  restabs  23287  restcls  23303  restntr  23304  hausnei2  23475  cmpsublem  23521  bwth  23532  hausmapdom  23622  ptpjcn  23733  upxp  23745  ptrescn  23761  xkopjcn  23778  fbssfi  23959  snfil  23986  ufprim  24031  rnelfm  24075  flimrest  24105  fclsrest  24146  tmdgsum  24217  blpnfctr  24558  mscl  24583  xmscl  24584  xmsge0  24585  xmseq0  24586  restmetu  24692  ngpds  24726  tngngp3  24778  unitnmn0  24790  xrsxmet  24932  metds0  24973  mpomulcn  24991  cncfmptc  25036  isclmp  25221  cnlmod  25264  ncvsi  25275  cphsqrtcl  25308  cfil3i  25393  cfilres  25420  cmssmscld  25474  cmmbl  25658  voliunlem2  25675  itg2ub  25857  itgrecl  25922  r1pid  26283  eflogeq  26729  cxpadd  26806  cxpcom  26866  logbchbase  26898  relogbreexp  26902  relogbzexp  26903  relogbmulexp  26905  logbleb  26910  logblt  26911  lawcos  26943  pythag  26944  asinsinb  27024  acoscosb  27025  atantanb  27051  amgmlem  27116  lgsneg  27447  lgsne0  27461  lgsmodeq  27468  lgsmulsqcoprm  27469  gausslemma2dlem1a  27491  2sqreulem2  27578  ltsres  27788  noetainflem1  27863  ltlestr  27886  lestr  27888  nocvxmin  27910  madebdaylemold  28053  lrrecpo  28096  ltadds2im  28141  leadds1im  28142  leadds2im  28143  leadds1  28144  leadds2  28145  ltadds1  28147  addscan2  28148  addscan1  28149  subadds  28225  ltsubs1  28231  divscl  28378  oncutlt  28419  zsoring  28564  expscllem  28585  brbtwn2  29192  colinearalg  29197  eleesubd  29199  axcgrrflx  29201  axcgrtr  29202  axsegcon  29214  ax5seglem1  29215  ax5seglem2  29216  ax5seglem4  29219  axbtwnid  29226  axlowdimlem14  29242  axlowdim  29248  axcontlem5  29255  axcontlem7  29257  nb3grprlem2  29668  cplgr3v  29722  cusgrsizeindslem  29738  sizusglecusglem2  29749  umgr2v2e  29812  cusgrrusgr  29868  iswlk  29897  edginwlk  29921  uspgr2wlkeq  29932  uspgr2wlkeq2  29933  uspgr2wlkeqi  29934  wlkonprop  29943  wlkon2n0  29951  pthdadjvtx  30014  upgr2pthnlp  30018  spthonepeq  30038  pthdlem2lem  30053  crctcshwlkn0lem3  30098  crctcshwlkn0lem5  30100  wlkiswwlks2lem4  30158  wlkiswwlks2lem6  30160  wlklnwwlkln2lem  30168  wwlksnred  30178  wwlksnextbi  30180  wwlksnextwrd  30183  2pthdlem1  30216  2wlkdlem10  30221  umgr2adedgwlkonALT  30233  elwwlks2s3  30237  elwwlks2ons3im  30240  s3wwlks2on  30242  sps3wwlks2on  30243  2wspdisj  30251  2wspiundisj  30252  clwwlkgt0  30274  clwlkclwwlklem2a4  30285  clwlkclwwlklem2a  30286  clwlkclwwlk  30290  clwlkclwwlk2  30291  clwlkclwwlkfo  30297  clwwisshclwwslemlem  30301  erclwwlktr  30310  clwwlkf  30335  wwlksubclwwlk  30346  erclwwlkntr  30359  clwwlknon  30378  frcond1  30554  frgr3v  30563  3vfriswmgr  30566  frgrwopreglem4a  30598  frrusgrord0lem  30627  clwwnonrepclwwnon  30633  extwwlkfab  30640  numclwwlk1lem2f1  30645  numclwwlk1lem2fo  30646  clwlknon2num  30656  numclwwlk2lem1  30664  numclwlk2lem2f  30665  numclwlk2lem2f1o  30667  numclwwlk2  30669  frgrreggt1  30681  friendshipgt3  30686  imsmetlem  30979  nmoxr  31055  nmoolb  31060  blometi  31092  phpar2  31112  phpar  31113  ipasslem5  31124  hvadd32  31323  hvaddsub12  31327  hvaddsubass  31330  hvsubass  31333  hvsub32  31334  hvsubdistr1  31338  hvsubdistr2  31339  hvmulcan  31361  hvmulcan2  31362  hvsubcan  31363  his5  31375  his2sub  31381  hhssabloilem  31550  hhssnv  31553  shlej2  31650  pjoi0  32006  hodcl  32036  hoadd32  32072  hosubdi  32097  hosubsub2  32101  hoaddsubass  32104  hosubsub4  32107  nmoplb  32196  unop  32204  hmop  32211  nmfnlb  32213  lnopmul  32256  kbass1  32405  kbass2  32406  leopmul2i  32424  leoptr  32426  cvntr  32581  mdslmd4i  32622  mdexchi  32624  atcv1  32669  sumdmdii  32704  fcoinvbr  32887  fpwrelmapffs  33016  xreceu  33178  isinftm  33438  inlidl  33669  unitdivcld  34232  esummulc1  34412  hasheuni  34416  unelsiga  34465  inelpisys  34485  carsgsigalem  34646  signswmnd  34885  bnj545  35224  bnj594  35241  bnj1311  35353  fissorduni  35419  r1filimi  35435  fineqvac  35448  fineqvnttrclselem3  35455  fineqvinfep  35457  usgrgt2cycl  35517  subgrwlk  35519  acycgr1v  35536  cvmsf1o  35659  cvmscld  35660  satefvfmla1  35812  elnanelprv  35816  lediv2aALT  36064  gcd32  36136  fununiq  36156  dfrdg4  36338  brcolinear  36446  colinearex  36447  nn0prpwlem  36718  clsun  36724  fnemeet1  36762  fnemeet2  36763  fnejoin1  36764  fnejoin2  36765  eltail  36770  rdgeqoa  37899  nlpineqsn  37937  curf  38132  lindsadd  38147  poimirlem28  38182  cnambfre  38202  ftc1anclem4  38230  cocanfo  38253  f1ocan1fv  38260  metf1o  38289  ismtybnd  38341  ghomco  38425  isdrngo2  38492  inidl  38564  igenmin  38598  brxrn  38917  brredunds  39244  cmtvalN  39870  cvrval  39928  pmapmeet  40432  paddval  40457  paddssat  40473  elpcliN  40552  pclssN  40553  pclunN  40557  paddunN  40586  poldmj1N  40587  tendoplcl2  41437  tendoplcl  41440  dihmeet  42002  lcmineqlem1  42681  reltsub1  43032  reltsubadd2  43033  resubsub4  43035  reppncan  43039  resubdi  43042  readdcan2  43059  subresre  43077  mapco2g  43332  mzpcompact2lem  43369  eqrabdioph  43395  lerabdioph  43419  eluzrabdioph  43420  ltrabdioph  43422  nerabdioph  43423  dvdsrabdioph  43424  reglogcl  43504  rmxyadd  43535  rmyabs  43572  congadd  43580  congabseq  43588  rmydioph  43628  mendring  43802  mendlmod  43803  iocinico  43826  omge1  43911  relexp0a  44329  relexpaddss  44331  brcoffn  44643  ismnushort  44898  dvconstbi  44931  uzwo4  45660  ssin0  45662  ssinc  45692  ssdec  45693  fvmpt2bd  45775  disjf1o  45796  ssnnf1octb  45799  sub31  45896  fperiodmullem  45909  ssfiunibd  45915  infxr  45969  fmul01  46183  islptre  46222  lptre2pt  46241  limcleqr  46245  limclner  46252  limsuppnflem  46311  limsupvaluz2  46339  supcnvlimsup  46341  xlimmnfvlem2  46434  xlimmnfv  46435  xlimpnfvlem2  46438  xlimpnfv  46439  climxlim2lem  46446  coskpi2  46467  cosknegpi  46470  dvnmptdivc  46539  dvdsn1add  46540  dvnmptconst  46542  dvmptfprod  46546  dvnprodlem1  46547  dvnprodlem2  46548  ovolsplit  46589  stoweidlem60  46661  stowei  46665  dirkeritg  46703  fourierdlem70  46777  fourierdlem71  46778  fourierdlem103  46810  fourierdlem104  46811  fouriersw  46832  rrxtopnfi  46888  saluncl  46918  salexct  46935  sge0ltfirp  47001  sge0iunmpt  47019  meadjiunlem  47066  meaiuninc3v  47085  carageniuncllem1  47122  caratheodorylem1  47127  ovncvrrp  47165  ovnsubaddlem1  47171  hspmbllem2  47228  ovolval5lem3  47255  smfpimbor1lem1  47399  smfsuplem1  47412  smflimsuplem4  47424  sigarls  47458  cnambpcma  47915  elfzelfzlble  47942  submodaddmod  47968  difltmodne  47969  m1mod0mod1  47981  modmkpkne  47988  mod2addne  47991  modm2nep1  47993  modm1nep2  47995  modm1nem2  47996  fsumsplitsndif  48002  fundcmpsurinjALT  48045  iccpartiltu  48055  prproropf1olem2  48137  fmtno4prmfac  48208  2pwp1prmfmtno  48226  lighneallem4b  48245  nprmdvdsfacm1lem4  48259  mogoldbblem  48369  gbegt5  48410  sbgoldbm  48433  nnsum3primesle9  48443  nnsum4primesodd  48445  nnsum4primesoddALTV  48446  evengpoap3  48448  nnsum4primesevenALTV  48450  clnbgredg  48489  opstrgric  48575  clnbgrgrimlem  48582  grtrif1o  48591  isubgr3stgrlem1  48615  isubgr3stgrlem4  48618  gpgusgralem  48705  gpg3nbgrvtx0  48725  isupwlk  48785  lidldomnnring  48885  2zrngacmnd  48897  rhmsubcALTVlem2  48931  fprmappr  49005  zlmodzxzscm  49017  gsumlsscl  49040  lincvalsng  49076  lincvalpr  49078  lincdifsn  49084  linc1  49085  lincellss  49086  fdivmpt  49200  digexp  49267  2arymaptfo  49314  line  49392  rrxline  49394  itsclc0xyqsolr  49429  iscnrm3r  49606  resipos  49633  amgmwlem  50471