Theorem 3adant1 1148

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3ad2ant2  1152  3ad2ant3  1153  3simpc  1168  eupickb  2661  spc3egv  3558  reuhyp  5382  predtrss  6324  onunel  6469  funopg  6572  funprg  6592  funtpg  6593  funcnvtp  6601  unima  6958  fvun1  6974  fnreseql  7045  xpprsng  7140  ftpg  7158  f1ounsn  7278  f13dfv  7280  f1ocoima  7309  f1ofvswap  7312  mpoeq3ia  7496  ordunel  7836  fex2  7946  funexw  7962  poxp  8138  poxp2  8153  poxp3  8160  poseq  8168  suppval1  8176  wfr3g  8330  smores3  8354  oaord  8548  oacan  8549  oaword  8550  omord  8569  omcan  8570  omwordri  8573  odi  8580  omass  8581  oeord  8590  oecan  8591  oewordri  8594  oeordsuc  8596  nnaord  8621  nnaordr  8622  nndi  8625  nnmass  8626  nnaword  8629  nnmord  8634  nnmwordri  8638  naddelim  8689  naddel1  8690  naddel2  8691  naddss1  8692  naddss2  8693  naddasslem2  8698  nadd32  8700  erov  8828  ecopovtrn  8834  curf  8883  ixpf  8941  f1oen4g  8984  f1dom4g  8985  mapxpen  9155  ssfi  9181  sbthfilem  9206  sbthfi  9207  onomeneq  9222  fimax2g  9270  fissorduni  9275  unbnn  9281  funisfsupp  9352  inelfi  9403  elfiun  9415  sup0  9452  suppr  9457  infpr  9490  ttrclss  9714  frr3g  9753  r111  9775  r1filimi  9896  dif1card  10082  ackbij1lem16  10305  cff1  10329  cfflb  10330  cfsmolem  10341  fin23lem34  10417  hsmexlem2  10498  axcc3  10509  domtriomlem  10513  axdc3lem4  10524  axdc4lem  10526  axcclem  10528  konigthlem  10646  gchdomtri  10707  tskpr  10848  tskop  10849  tskuni  10861  tskun  10864  gruop  10883  gruun  10884  grudomon  10895  adderpqlem  11032  mulerpqlem  11033  addassnq  11036  mulassnq  11037  distrnq  11039  ltsonq  11047  ltanq  11049  ltmnq  11050  genpass  11087  distrlem1pr  11103  distrlem4pr  11104  ltsopr  11110  adddir  11290  axlttrn  11375  ltletr  11395  letr  11397  mul32  11469  mul31  11470  add32  11522  subsub23  11555  addsubass  11560  subcan2  11576  subsub2  11579  nppcan2  11582  sub32  11585  nnncan  11586  nnncan2  11588  pnpcan2  11591  subdi  11742  subdir  11743  receu  11954  mulcan1g  11962  mulcan2g  11963  divmul3  11972  divrec  11983  divrec2  11984  div11  11995  divsubdir  12003  subdivcomb2  12006  divdiv1  12021  redivcl  12029  div2neg  12033  ltmul2  12161  lemul1  12162  lemul2  12163  lemul2a  12165  lediv1  12175  gt0div  12176  ge0div  12177  mulsuble0b  12182  ltdivmul  12185  ledivmul  12186  ltdivmul2  12187  ledivmul2  12189  lemuldiv  12190  ltdiv23  12201  lediv23  12202  ledivp1i  12235  ltdivp1i  12236  uzind2  12785  nn0ind  12787  fnn0ind  12791  uz3m2nn  13014  xrltletr  13279  xrletr  13280  xrre2  13293  xrltmin  13305  xrlemin  13307  xleadd2a  13377  xleadd1  13378  xltadd2  13380  xmulasslem3  13409  xmulass  13410  xltmul2  13416  ixxdisj  13484  iooneg  13595  iccneg  13596  icoshft  13597  icoshftf1o  13598  icodisj  13600  snunioo  13602  fzen  13667  ssfzunsnext  13696  fzrev3  13717  2ffzeq  13776  fzoaddel2  13848  elfzodifsumelfzo  13859  ssfzoulel  13888  ssfzo12bi  13889  fzoopth  13890  fzoshftral  13915  adddivflid  13951  flltdivnn0lt  13966  ltdifltdiv  13967  fldiv4p1lem1div2  13968  modcyc  14039  modcyc2  14040  modaddabs  14044  muladdmod  14048  modsubmodmod  14066  modaddmodup  14070  modaddmulmod  14074  moddi  14075  modsubdir  14076  expdiv  14249  digit2  14373  nfile  14496  hashdifpr  14553  hashgt23el  14562  hashreshashfun  14577  hashf1dmcdm  14582  hash3tpexb  14632  fi1uzind  14645  ccatval1  14715  ccatass  14727  swrdval  14784  swrdnd  14797  swrd0  14801  swrdfv2  14804  pfxsuff1eqwrdeq  14841  swrdswrdlem  14846  pfxccatin12lem2a  14869  pfxccatin12lem1  14870  repswccat  14930  cshwidxmod  14947  cshwidxmodr  14948  cshf1  14954  repswcshw  14956  2cshw  14957  2cshwcom  14960  2cshwcshw  14969  cshwcsh2id  14972  ccatco  14979  2swrd2eqwrdeq  15099  wwlktovf  15102  brcnvtrclfv  15149  shftval2  15221  mulre  15281  absdiv  15455  absdiflt  15478  absdifle  15479  abs3dif  15492  cau3  15516  ello12r  15677  elo12r  15688  modfsummods  15953  geoisum1c  16042  rpnnen2lem4  16378  rpnnen2lem7  16381  addmulmodb  16428  dvdsmulc  16446  dvdsmulcr  16448  dvdsmultr1  16459  dvdsmultr2  16461  dvdssub2  16464  oexpneg  16508  divalgb  16567  ndvdsadd  16573  sadass  16634  modgcd  16698  dvdsgcd  16710  dvdsgcdb  16711  gcdass  16713  mulgcd  16714  absmulgcd  16715  rpmulgcd  16724  expgcd  16730  zexpgcd  16732  nn0seqcvgd  16738  algcvga  16747  lcmdvdsb  16781  lcmass  16782  lcmfunsnlem1  16805  lcmfunsnlem2lem1  16806  lcmfunsnlem2lem2  16807  coprmdvds  16821  coprmdvds2  16822  rpmul  16827  cncongr1  16835  cncongr2  16836  qnumdenbi  16913  modprm0  16976  coprimeprodsq  16979  pythagtriplem4  16990  pythagtriplem8  16994  pythagtriplem9  16995  pythagtriplem12  16997  pythagtriplem14  16999  pythagtriplem16  17001  pcpremul  17014  pcgcd  17049  vdwapval  17144  vdwapun  17145  prmgaplem3  17224  prmgaplem4  17225  prmgaplem7  17228  prmgapprmolem  17232  mreiincl  17759  mreincl  17762  mremre  17767  mrcss  17783  catcisolem  18278  pleval2  18502  pospo  18510  latlem  18604  latjcom  18614  latmcom  18630  lubss  18680  lubun  18682  clatglbss  18686  ipole  18701  ipolt  18702  pslem  18739  dirtr  18769  gsumsgrpccat  19029  gsumws2  19031  frmdmnd  19048  symggrplem  19073  isgrpi  19163  grpsubrcan  19224  grpinvsub  19225  grpsubeq0  19229  grpsubadd0sub  19230  grpnpcan  19235  qussub  19399  ghmsub  19431  symgpssefmnd  19603  symggrp  19607  symgextsymg  19631  gsmsymgreqlem2  19638  symgfixfolem1  19645  pmtrprfv3  19661  symggen  19677  lsmass  19876  efgsrel  19941  cntzcmn  20047  dvrcl  20627  unitdvcl  20628  dvrcan1  20632  subrngmre  20807  subrgmre  20842  rhmsubclem2  20931  rrgeq0  20945  abvsubtri  21077  abvtrivd  21082  lmodvsubval2  21185  rmodislmodlem  21197  rmodislmod  21198  lss0cl  21215  lssintcl  21232  lssincl  21233  reslmhm2  21321  lspvadd  21364  lspsntrim  21366  islbs3  21426  unichnlidl  21509  rnglidlmmgm  21526  cncrng  21692  xrsmcmn  21694  cndrng  21700  cnsrng  21705  absabv  21723  xrs1mnd  21739  psgnco  21882  zrhpsgninv  21884  zrhpsgnevpm  21890  zrhpsgnodpm  21891  zrhpsgnelbas  21893  zrhcopsgnelbas  21894  uvcresum  22092  lindfmm  22126  lindsmm  22127  evlsval2  22389  mamudm  22703  mamufacex  22704  matsubgcell  22742  matsc  22758  scmatscmide  22815  scmatrhmcl  22836  1marepvsma1  22891  m1detdiag  22905  mdetralt  22916  m2detleiblem7  22935  gsummatr01lem3  22965  gsummatr01  22967  smadiadetlem0  22969  decpmate  23077  decpmatcl  23078  pm2mpcl  23108  pm2mpghmlem2  23123  chfacfscmul0  23169  chfacfscmulgsum  23171  chfacfpmmul0  23173  chfacfpmmulgsum  23175  unopn  23214  clsss  23365  cldmre  23389  toponmre  23404  opnssneib  23426  restabs  23476  restcls  23492  restntr  23493  hausnei2  23664  cmpsublem  23710  bwth  23721  hausmapdom  23812  ptpjcn  23923  upxp  23935  ptrescn  23951  xkopjcn  23968  fbssfi  24149  snfil  24176  ufprim  24221  rnelfm  24265  flimrest  24295  fclsrest  24336  tmdgsum  24407  blpnfctr  24748  mscl  24773  xmscl  24774  xmsge0  24775  xmseq0  24776  restmetu  24882  ngpds  24916  tngngp3  24968  unitnmn0  24980  xrsxmet  25122  metds0  25163  mpomulcn  25181  cncfmptc  25226  isclmp  25411  cnlmod  25454  ncvsi  25465  cphsqrtcl  25498  cfil3i  25583  cfilres  25610  cmssmscld  25664  cmmbl  25848  voliunlem2  25865  itg2ub  26047  itgrecl  26111  r1pid  26472  eflogeq  26923  cxpadd  27000  cxpcom  27060  logbchbase  27092  relogbreexp  27096  relogbzexp  27097  relogbmulexp  27099  logbleb  27104  logblt  27105  lawcos  27137  pythag  27138  asinsinb  27218  acoscosb  27219  atantanb  27245  amgmlem  27310  lgsneg  27641  lgsne0  27655  lgsmodeq  27662  lgsmulsqcoprm  27663  gausslemma2dlem1a  27685  2sqreulem2  27772  ltsres  28012  noetainflem1  28087  ltlestr  28110  lestr  28112  nocvxmin  28134  madebdaylemold  28277  lrrecpo  28320  ltadds2im  28365  leadds1im  28366  leadds2im  28367  leadds1  28368  leadds2  28369  ltadds1  28371  addscan2  28372  addscan1  28373  subadds  28449  ltsubs1  28455  divscl  28602  oncutlt  28643  zsoring  28788  expscllem  28809  brbtwn2  29476  colinearalg  29481  eleesubd  29483  axcgrrflx  29485  axcgrtr  29486  axsegcon  29498  ax5seglem1  29499  ax5seglem2  29500  ax5seglem4  29503  axbtwnid  29510  axlowdimlem14  29526  axlowdim  29532  axcontlem5  29539  axcontlem7  29541  nb3grprlem2  29955  cplgr3v  30009  cusgrsizeindslem  30025  sizusglecusglem2  30036  umgr2v2e  30099  cusgrrusgr  30155  iswlk  30184  edginwlk  30208  uspgr2wlkeq  30219  uspgr2wlkeq2  30220  uspgr2wlkeqi  30221  wlkonprop  30230  wlkon2n0  30238  subgrwlk  30262  pthdadjvtx  30306  upgr2pthnlp  30311  spthonepeq  30331  pthdlem2lem  30346  crctcshwlkn0lem3  30394  crctcshwlkn0lem5  30396  wlkiswwlks2lem4  30454  wlkiswwlks2lem6  30456  wlklnwwlkln2lem  30464  wwlksnred  30474  wwlksnextbi  30476  wwlksnextwrd  30479  2pthdlem1  30512  2wlkdlem10  30517  umgr2adedgwlkonALT  30529  elwwlks2s3  30533  elwwlks2ons3im  30536  s3wwlks2on  30538  sps3wwlks2on  30539  2wspdisj  30547  2wspiundisj  30548  clwwlkgt0  30570  clwlkclwwlklem2a4  30581  clwlkclwwlklem2a  30582  clwlkclwwlk  30586  clwlkclwwlk2  30587  clwlkclwwlkfo  30593  clwwisshclwwslemlem  30597  erclwwlktr  30606  clwwlkf  30631  wwlksubclwwlk  30642  erclwwlkntr  30655  clwwlknon  30674  frcond1  30860  frgr3v  30869  3vfriswmgr  30872  frgrwopreglem4a  30904  frrusgrord0lem  30933  clwwnonrepclwwnon  30939  extwwlkfab  30946  numclwwlk1lem2f1  30951  numclwwlk1lem2fo  30952  clwlknon2num  30962  numclwwlk2lem1  30970  numclwlk2lem2f  30971  numclwlk2lem2f1o  30973  numclwwlk2  30975  frgrreggt1  30987  friendshipgt3  30992  imsmetlem  31285  nmoxr  31361  nmoolb  31366  blometi  31398  phpar2  31418  phpar  31419  ipasslem5  31430  hvadd32  31629  hvaddsub12  31633  hvaddsubass  31636  hvsubass  31639  hvsub32  31640  hvsubdistr1  31644  hvsubdistr2  31645  hvmulcan  31667  hvmulcan2  31668  hvsubcan  31669  his5  31681  his2sub  31687  hhssabloilem  31856  hhssnv  31859  shlej2  31956  pjoi0  32312  hodcl  32342  hoadd32  32378  hosubdi  32403  hosubsub2  32407  hoaddsubass  32410  hosubsub4  32413  nmoplb  32502  unop  32510  hmop  32517  nmfnlb  32519  lnopmul  32562  kbass1  32711  kbass2  32712  leopmul2i  32730  leoptr  32732  cvntr  32887  mdslmd4i  32928  mdexchi  32930  atcv1  32975  sumdmdii  33010  fcoinvbr  33192  fpwrelmapffs  33319  xreceu  33481  isinftm  33735  inlidl  33964  unitdivcld  34526  esummulc1  34706  hasheuni  34710  unelsiga  34759  inelpisys  34780  carsgsigalem  34940  signswmnd  35179  bnj545  35518  bnj594  35535  bnj1311  35647  fineqvac  35767  fineqvnttrclselem3  35774  fineqvinfep  35776  usgrgt2cycl  35888  acycgr1v  35893  cvmsf1o  36016  cvmscld  36017  satefvfmla1  36169  elnanelprv  36173  lediv2aALT  36421  gcd32  36493  fununiq  36513  dfrdg4  36695  brcolinear  36804  colinearex  36805  ltnmul  36945  ltnadd  36947  nn0prpwlem  37090  clsun  37096  fnemeet1  37134  fnemeet2  37135  fnejoin1  37136  fnejoin2  37137  eltail  37142  rdgeqoa  38273  nlpineqsn  38311  lindsadd  38516  poimirlem28  38546  cnambfre  38566  ftc1anclem4  38594  cocanfo  38633  f1ocan1fv  38640  metf1o  38669  ismtybnd  38721  ghomco  38805  isdrngo2  38872  inidl  38944  igenmin  38978  brxrn  39295  brredunds  39622  cmtvalN  40248  cvrval  40306  pmapmeet  40810  paddval  40835  paddssat  40851  elpcliN  40930  pclssN  40931  pclunN  40935  paddunN  40964  poldmj1N  40965  tendoplcl2  41815  tendoplcl  41818  dihmeet  42380  lcmineqlem1  43059  reltsub1  43417  reltsubadd2  43418  resubsub4  43420  reppncan  43424  resubdi  43427  readdcan2  43444  subresre  43462  mapco2g  43704  mzpcompact2lem  43741  eqrabdioph  43767  lerabdioph  43791  eluzrabdioph  43792  ltrabdioph  43794  nerabdioph  43795  dvdsrabdioph  43796  reglogcl  43876  rmxyadd  43907  rmyabs  43944  congadd  43952  congabseq  43960  rmydioph  44000  mendring  44174  mendlmod  44175  iocinico  44198  omge1  44283  relexp0a  44701  relexpaddss  44703  brcoffn  45015  ismnushort  45270  dvconstbi  45303  uzwo4  46039  ssin0  46041  ssinc  46071  ssdec  46072  fvmpt2bd  46154  disjf1o  46175  ssnnf1octb  46178  sub31  46275  fperiodmullem  46288  ssfiunibd  46294  infxr  46347  fmul01  46561  islptre  46600  lptre2pt  46619  limcleqr  46623  limclner  46630  limsuppnflem  46689  limsupvaluz2  46717  supcnvlimsup  46719  xlimmnfvlem2  46812  xlimmnfv  46813  xlimpnfvlem2  46816  xlimpnfv  46817  climxlim2lem  46824  coskpi2  46845  cosknegpi  46848  dvnmptdivc  46917  dvdsn1add  46918  dvnmptconst  46920  dvmptfprod  46924  dvnprodlem1  46925  dvnprodlem2  46926  ovolsplit  46967  stoweidlem60  47039  stowei  47043  dirkeritg  47081  fourierdlem70  47155  fourierdlem71  47156  fourierdlem103  47188  fourierdlem104  47189  fouriersw  47210  rrxtopnfi  47266  saluncl  47296  salexct  47313  sge0ltfirp  47379  sge0iunmpt  47397  meadjiunlem  47444  meaiuninc3v  47463  carageniuncllem1  47500  caratheodorylem1  47505  ovncvrrp  47543  ovnsubaddlem1  47549  hspmbllem2  47606  ovolval5lem3  47633  smfpimbor1lem1  47777  smfsuplem1  47790  smflimsuplem4  47802  sigarls  47836  cnambpcma  48333  elfzelfzlble  48360  submodaddmod  48386  difltmodne  48387  m1mod0mod1  48399  modmkpkne  48406  mod2addne  48409  modm2nep1  48411  modm1nep2  48413  modm1nem2  48414  fsumsplitsndif  48420  fundcmpsurinjALT  48463  iccpartiltu  48473  prproropf1olem2  48555  fmtno4prmfac  48626  2pwp1prmfmtno  48644  lighneallem4b  48663  nprmdvdsfacm1lem4  48677  mogoldbblem  48787  gbegt5  48828  sbgoldbm  48851  nnsum3primesle9  48861  nnsum4primesodd  48863  nnsum4primesoddALTV  48864  evengpoap3  48866  nnsum4primesevenALTV  48868  clnbgredg  48907  opstrgric  48993  clnbgrgrimlem  49000  grtrif1o  49009  isubgr3stgrlem1  49033  isubgr3stgrlem4  49036  gpgusgralem  49123  gpg3nbgrvtx0  49143  isupwlk  49203  lidldomnnring  49302  2zrngacmnd  49314  rhmsubcALTVlem2  49348  fprmappr  49426  zlmodzxzscm  49438  gsumlsscl  49461  lincvalsng  49497  lincvalpr  49499  lincdifsn  49505  linc1  49506  lincellss  49507  fdivmpt  49621  digexp  49688  2arymaptfo  49735  line  49813  rrxline  49815  itsclc0xyqsolr  49850  iscnrm3r  50025  resipos  50052  amgmwlem  50956