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

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

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 1105

This theorem is referenced by:  3ad2ant2  1152  3ad2ant3  1153  3simpc  1168  eupickb  2663  spc3egv  3562  reuhyp  5391  predtrss  6323  onunel  6468  funopg  6570  funprg  6590  funtpg  6591  funcnvtp  6599  unima  6956  fvun1  6972  fnreseql  7043  xpprsng  7136  ftpg  7153  f1ounsn  7270  f13dfv  7272  f1ocoima  7301  f1ofvswap  7304  mpoeq3ia  7488  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  10237  cfflb  10238  cfsmolem  10249  fin23lem34  10325  hsmexlem2  10406  axcc3  10417  domtriomlem  10421  axdc3lem4  10432  axdc4lem  10434  axcclem  10436  konigthlem  10548  gchdomtri  10609  tskpr  10750  tskop  10751  tskuni  10763  tskun  10766  gruop  10785  gruun  10786  grudomon  10797  adderpqlem  10934  mulerpqlem  10935  addassnq  10938  mulassnq  10939  distrnq  10941  ltsonq  10949  ltanq  10951  ltmnq  10952  genpass  10989  distrlem1pr  11005  distrlem4pr  11006  ltsopr  11012  adddir  11192  axlttrn  11277  ltletr  11297  letr  11299  mul32  11371  mul31  11372  add32  11424  subsub23  11457  addsubass  11462  subcan2  11478  subsub2  11481  nppcan2  11484  sub32  11487  nnncan  11488  nnncan2  11490  pnpcan2  11493  subdi  11642  subdir  11643  receu  11854  mulcan1g  11862  mulcan2g  11863  divmul3  11872  divrec  11883  divrec2  11884  div11  11895  divsubdir  11903  subdivcomb2  11906  divdiv1  11921  redivcl  11929  div2neg  11933  ltmul2  12061  lemul1  12062  lemul2  12063  lemul2a  12065  lediv1  12075  gt0div  12076  ge0div  12077  mulsuble0b  12082  ltdivmul  12085  ledivmul  12086  ltdivmul2  12087  ledivmul2  12089  lemuldiv  12090  ltdiv23  12101  lediv23  12102  ledivp1i  12135  ltdivp1i  12136  uzind2  12684  nn0ind  12686  fnn0ind  12690  uz3m2nn  12913  xrltletr  13177  xrletr  13178  xrre2  13191  xrltmin  13203  xrlemin  13205  xleadd2a  13275  xleadd1  13276  xltadd2  13278  xmulasslem3  13307  xmulass  13308  xltmul2  13314  ixxdisj  13382  iooneg  13493  iccneg  13494  icoshft  13495  icoshftf1o  13496  icodisj  13498  snunioo  13500  fzen  13564  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  16268  rpnnen2lem7  16271  addmulmodb  16318  dvdsmulc  16336  dvdsmulcr  16338  dvdsmultr1  16349  dvdsmultr2  16351  dvdssub2  16354  oexpneg  16398  divalgb  16457  ndvdsadd  16463  sadass  16524  modgcd  16585  dvdsgcd  16597  dvdsgcdb  16598  gcdass  16600  mulgcd  16601  absmulgcd  16602  rpmulgcd  16610  expgcd  16616  zexpgcd  16618  nn0seqcvgd  16623  algcvga  16632  lcmdvdsb  16666  lcmass  16667  lcmfunsnlem1  16690  lcmfunsnlem2lem1  16691  lcmfunsnlem2lem2  16692  coprmdvds  16706  coprmdvds2  16707  rpmul  16712  cncongr1  16720  cncongr2  16721  qnumdenbi  16798  modprm0  16860  coprimeprodsq  16863  pythagtriplem4  16874  pythagtriplem8  16878  pythagtriplem9  16879  pythagtriplem12  16881  pythagtriplem14  16883  pythagtriplem16  16885  pcpremul  16898  pcgcd  16933  vdwapval  17028  vdwapun  17029  prmgaplem3  17108  prmgaplem4  17109  prmgaplem7  17112  prmgapprmolem  17116  mreiincl  17643  mreincl  17646  mremre  17651  mrcss  17667  catcisolem  18162  pleval2  18386  pospo  18394  latlem  18488  latjcom  18498  latmcom  18514  lubss  18564  lubun  18566  clatglbss  18570  ipole  18585  ipolt  18586  pslem  18623  dirtr  18653  gsumsgrpccat  18894  gsumws2  18896  frmdmnd  18913  symggrplem  18938  isgrpi  19021  grpsubrcan  19082  grpinvsub  19083  grpsubeq0  19087  grpsubadd0sub  19088  grpnpcan  19093  qussub  19257  ghmsub  19289  symgpssefmnd  19461  symggrp  19465  symgextsymg  19489  gsmsymgreqlem2  19496  symgfixfolem1  19503  pmtrprfv3  19519  symggen  19535  lsmass  19734  efgsrel  19799  cntzcmn  19905  dvrcl  20482  unitdvcl  20483  dvrcan1  20487  subrngmre  20661  subrgmre  20696  rhmsubclem2  20785  rrgeq0  20799  abvsubtri  20930  abvtrivd  20935  lmodvsubval2  21038  rmodislmodlem  21050  rmodislmod  21051  lss0cl  21068  lssintcl  21085  lssincl  21086  reslmhm2  21174  lspvadd  21217  lspsntrim  21219  islbs3  21279  unichnlidl  21362  rnglidlmmgm  21379  cncrng  21543  xrsmcmn  21545  cndrng  21551  cnsrng  21556  absabv  21574  xrs1mnd  21590  psgnco  21733  zrhpsgninv  21735  zrhpsgnevpm  21741  zrhpsgnodpm  21742  zrhpsgnelbas  21744  zrhcopsgnelbas  21745  uvcresum  21943  lindfmm  21977  lindsmm  21978  evlsval2  22238  mamudm  22552  mamufacex  22553  matsubgcell  22591  matsc  22607  scmatscmide  22664  scmatrhmcl  22685  1marepvsma1  22740  m1detdiag  22754  mdetralt  22765  m2detleiblem7  22784  gsummatr01lem3  22814  gsummatr01  22816  smadiadetlem0  22818  decpmate  22923  decpmatcl  22924  pm2mpcl  22954  pm2mpghmlem2  22969  chfacfscmul0  23015  chfacfscmulgsum  23017  chfacfpmmul0  23019  chfacfpmmulgsum  23021  unopn  23060  clsss  23211  cldmre  23235  toponmre  23250  opnssneib  23272  restabs  23322  restcls  23338  restntr  23339  hausnei2  23510  cmpsublem  23556  bwth  23567  hausmapdom  23657  ptpjcn  23768  upxp  23780  ptrescn  23796  xkopjcn  23813  fbssfi  23994  snfil  24021  ufprim  24066  rnelfm  24110  flimrest  24140  fclsrest  24181  tmdgsum  24252  blpnfctr  24593  mscl  24618  xmscl  24619  xmsge0  24620  xmseq0  24621  restmetu  24727  ngpds  24761  tngngp3  24813  unitnmn0  24825  xrsxmet  24967  metds0  25008  mpomulcn  25026  cncfmptc  25071  isclmp  25256  cnlmod  25299  ncvsi  25310  cphsqrtcl  25343  cfil3i  25428  cfilres  25455  cmssmscld  25509  cmmbl  25693  voliunlem2  25710  itg2ub  25892  itgrecl  25957  r1pid  26318  eflogeq  26767  cxpadd  26844  cxpcom  26904  logbchbase  26936  relogbreexp  26940  relogbzexp  26941  relogbmulexp  26943  logbleb  26948  logblt  26949  lawcos  26981  pythag  26982  asinsinb  27062  acoscosb  27063  atantanb  27089  amgmlem  27154  lgsneg  27485  lgsne0  27499  lgsmodeq  27506  lgsmulsqcoprm  27507  gausslemma2dlem1a  27529  2sqreulem2  27616  ltsres  27826  noetainflem1  27901  ltlestr  27924  lestr  27926  nocvxmin  27948  madebdaylemold  28091  lrrecpo  28134  ltadds2im  28179  leadds1im  28180  leadds2im  28181  leadds1  28182  leadds2  28183  ltadds1  28185  addscan2  28186  addscan1  28187  subadds  28263  ltsubs1  28269  divscl  28416  oncutlt  28457  zsoring  28602  expscllem  28623  brbtwn2  29255  colinearalg  29260  eleesubd  29262  axcgrrflx  29264  axcgrtr  29265  axsegcon  29277  ax5seglem1  29278  ax5seglem2  29279  ax5seglem4  29282  axbtwnid  29289  axlowdimlem14  29305  axlowdim  29311  axcontlem5  29318  axcontlem7  29320  nb3grprlem2  29731  cplgr3v  29785  cusgrsizeindslem  29801  sizusglecusglem2  29812  umgr2v2e  29875  cusgrrusgr  29931  iswlk  29960  edginwlk  29984  uspgr2wlkeq  29995  uspgr2wlkeq2  29996  uspgr2wlkeqi  29997  wlkonprop  30006  wlkon2n0  30014  pthdadjvtx  30077  upgr2pthnlp  30081  spthonepeq  30101  pthdlem2lem  30116  crctcshwlkn0lem3  30161  crctcshwlkn0lem5  30163  wlkiswwlks2lem4  30221  wlkiswwlks2lem6  30223  wlklnwwlkln2lem  30231  wwlksnred  30241  wwlksnextbi  30243  wwlksnextwrd  30246  2pthdlem1  30279  2wlkdlem10  30284  umgr2adedgwlkonALT  30296  elwwlks2s3  30300  elwwlks2ons3im  30303  s3wwlks2on  30305  sps3wwlks2on  30306  2wspdisj  30314  2wspiundisj  30315  clwwlkgt0  30337  clwlkclwwlklem2a4  30348  clwlkclwwlklem2a  30349  clwlkclwwlk  30353  clwlkclwwlk2  30354  clwlkclwwlkfo  30360  clwwisshclwwslemlem  30364  erclwwlktr  30373  clwwlkf  30398  wwlksubclwwlk  30409  erclwwlkntr  30422  clwwlknon  30441  frcond1  30617  frgr3v  30626  3vfriswmgr  30629  frgrwopreglem4a  30661  frrusgrord0lem  30690  clwwnonrepclwwnon  30696  extwwlkfab  30703  numclwwlk1lem2f1  30708  numclwwlk1lem2fo  30709  clwlknon2num  30719  numclwwlk2lem1  30727  numclwlk2lem2f  30728  numclwlk2lem2f1o  30730  numclwwlk2  30732  frgrreggt1  30744  friendshipgt3  30749  imsmetlem  31042  nmoxr  31118  nmoolb  31123  blometi  31155  phpar2  31175  phpar  31176  ipasslem5  31187  hvadd32  31386  hvaddsub12  31390  hvaddsubass  31393  hvsubass  31396  hvsub32  31397  hvsubdistr1  31401  hvsubdistr2  31402  hvmulcan  31424  hvmulcan2  31425  hvsubcan  31426  his5  31438  his2sub  31444  hhssabloilem  31613  hhssnv  31616  shlej2  31713  pjoi0  32069  hodcl  32099  hoadd32  32135  hosubdi  32160  hosubsub2  32164  hoaddsubass  32167  hosubsub4  32170  nmoplb  32259  unop  32267  hmop  32274  nmfnlb  32276  lnopmul  32319  kbass1  32468  kbass2  32469  leopmul2i  32487  leoptr  32489  cvntr  32644  mdslmd4i  32685  mdexchi  32687  atcv1  32732  sumdmdii  32767  fcoinvbr  32950  fpwrelmapffs  33079  xreceu  33241  isinftm  33501  inlidl  33729  unitdivcld  34291  esummulc1  34471  hasheuni  34475  unelsiga  34524  inelpisys  34544  carsgsigalem  34705  signswmnd  34944  bnj545  35283  bnj594  35300  bnj1311  35412  fissorduni  35480  r1filimi  35497  fineqvac  35529  fineqvnttrclselem3  35536  fineqvinfep  35538  usgrgt2cycl  35622  subgrwlk  35624  acycgr1v  35641  cvmsf1o  35764  cvmscld  35765  satefvfmla1  35917  elnanelprv  35921  lediv2aALT  36169  gcd32  36241  fununiq  36261  dfrdg4  36443  brcolinear  36551  colinearex  36552  ltnmul  36693  ltnadd  36695  nn0prpwlem  36833  clsun  36839  fnemeet1  36877  fnemeet2  36878  fnejoin1  36879  fnejoin2  36880  eltail  36885  rdgeqoa  38016  nlpineqsn  38054  curf  38249  lindsadd  38264  poimirlem28  38299  cnambfre  38319  ftc1anclem4  38347  cocanfo  38370  f1ocan1fv  38377  metf1o  38406  ismtybnd  38458  ghomco  38542  isdrngo2  38609  inidl  38681  igenmin  38715  brxrn  39032  brredunds  39359  cmtvalN  39985  cvrval  40043  pmapmeet  40547  paddval  40572  paddssat  40588  elpcliN  40667  pclssN  40668  pclunN  40672  paddunN  40701  poldmj1N  40702  tendoplcl2  41552  tendoplcl  41555  dihmeet  42117  lcmineqlem1  42796  reltsub1  43147  reltsubadd2  43148  resubsub4  43150  reppncan  43154  resubdi  43157  readdcan2  43174  subresre  43192  mapco2g  43445  mzpcompact2lem  43482  eqrabdioph  43508  lerabdioph  43532  eluzrabdioph  43533  ltrabdioph  43535  nerabdioph  43536  dvdsrabdioph  43537  reglogcl  43617  rmxyadd  43648  rmyabs  43685  congadd  43693  congabseq  43701  rmydioph  43741  mendring  43915  mendlmod  43916  iocinico  43939  omge1  44024  relexp0a  44442  relexpaddss  44444  brcoffn  44756  ismnushort  45011  dvconstbi  45044  uzwo4  45773  ssin0  45775  ssinc  45805  ssdec  45806  fvmpt2bd  45888  disjf1o  45909  ssnnf1octb  45912  sub31  46009  fperiodmullem  46022  ssfiunibd  46028  infxr  46082  fmul01  46296  islptre  46335  lptre2pt  46354  limcleqr  46358  limclner  46365  limsuppnflem  46424  limsupvaluz2  46452  supcnvlimsup  46454  xlimmnfvlem2  46547  xlimmnfv  46548  xlimpnfvlem2  46551  xlimpnfv  46552  climxlim2lem  46559  coskpi2  46580  cosknegpi  46583  dvnmptdivc  46652  dvdsn1add  46653  dvnmptconst  46655  dvmptfprod  46659  dvnprodlem1  46660  dvnprodlem2  46661  ovolsplit  46702  stoweidlem60  46774  stowei  46778  dirkeritg  46816  fourierdlem70  46890  fourierdlem71  46891  fourierdlem103  46923  fourierdlem104  46924  fouriersw  46945  rrxtopnfi  47001  saluncl  47031  salexct  47048  sge0ltfirp  47114  sge0iunmpt  47132  meadjiunlem  47179  meaiuninc3v  47198  carageniuncllem1  47235  caratheodorylem1  47240  ovncvrrp  47278  ovnsubaddlem1  47284  hspmbllem2  47341  ovolval5lem3  47368  smfpimbor1lem1  47512  smfsuplem1  47525  smflimsuplem4  47537  sigarls  47571  cnambpcma  48031  elfzelfzlble  48058  submodaddmod  48084  difltmodne  48085  m1mod0mod1  48097  modmkpkne  48104  mod2addne  48107  modm2nep1  48109  modm1nep2  48111  modm1nem2  48112  fsumsplitsndif  48118  fundcmpsurinjALT  48161  iccpartiltu  48171  prproropf1olem2  48253  fmtno4prmfac  48324  2pwp1prmfmtno  48342  lighneallem4b  48361  nprmdvdsfacm1lem4  48375  mogoldbblem  48485  gbegt5  48526  sbgoldbm  48549  nnsum3primesle9  48559  nnsum4primesodd  48561  nnsum4primesoddALTV  48562  evengpoap3  48564  nnsum4primesevenALTV  48566  clnbgredg  48605  opstrgric  48691  clnbgrgrimlem  48698  grtrif1o  48707  isubgr3stgrlem1  48731  isubgr3stgrlem4  48734  gpgusgralem  48821  gpg3nbgrvtx0  48841  isupwlk  48901  lidldomnnring  49001  2zrngacmnd  49013  rhmsubcALTVlem2  49047  fprmappr  49125  zlmodzxzscm  49137  gsumlsscl  49160  lincvalsng  49196  lincvalpr  49198  lincdifsn  49204  linc1  49205  lincellss  49206  fdivmpt  49320  digexp  49387  2arymaptfo  49434  line  49512  rrxline  49514  itsclc0xyqsolr  49549  iscnrm3r  49726  resipos  49753  amgmwlem  50622