Theorem 3adant1 1130

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3ad2ant2  1134  3ad2ant3  1135  3simpc  1150  eupickb  2628  spc3egv  3569  sbciegftOLD  3791  reuhyp  5375  predtrss  6295  onunel  6439  funopg  6550  funprg  6570  funtpg  6571  funcnvtp  6579  unima  6936  fvun1  6952  fnreseql  7020  xpprsng  7112  ftpg  7128  f1ounsn  7247  f13dfv  7249  f1ocoima  7278  f1ofvswap  7281  mpoeq3ia  7467  ordunel  7802  fex2  7912  funexw  7930  poxp  8107  poxp2  8122  poxp3  8129  poseq  8137  suppval1  8145  wfr3g  8298  smores3  8322  oaord  8511  oacan  8512  oaword  8513  omord  8532  omcan  8533  omwordri  8536  odi  8543  omass  8544  oeord  8552  oecan  8553  oewordri  8556  oeordsuc  8558  nnaord  8583  nnaordr  8584  nndi  8587  nnmass  8588  nnaword  8591  nnmord  8596  nnmwordri  8600  naddelim  8650  naddel1  8651  naddel2  8652  naddss1  8653  naddss2  8654  naddasslem2  8659  nadd32  8661  erov  8787  ecopovtrn  8793  ixpf  8893  f1oen4g  8936  f1dom4g  8937  mapxpen  9107  dif1enlemOLD  9121  ssfi  9137  sbthfilem  9162  sbthfi  9163  onomeneq  9178  fimax2g  9233  unbnn  9243  funisfsupp  9318  inelfi  9369  elfiun  9381  sup0  9418  suppr  9423  infpr  9456  ttrclss  9673  frr3g  9709  r111  9728  dif1card  9963  ackbij1lem16  10187  cff1  10211  cfflb  10212  cfsmolem  10223  fin23lem34  10299  hsmexlem2  10380  axcc3  10391  domtriomlem  10395  axdc3lem4  10406  axdc4lem  10408  axcclem  10410  konigthlem  10521  gchdomtri  10582  tskpr  10723  tskop  10724  tskuni  10736  tskun  10739  gruop  10758  gruun  10759  grudomon  10770  adderpqlem  10907  mulerpqlem  10908  addassnq  10911  mulassnq  10912  distrnq  10914  ltsonq  10922  ltanq  10924  ltmnq  10925  genpass  10962  distrlem1pr  10978  distrlem4pr  10979  ltsopr  10985  adddir  11165  axlttrn  11246  ltletr  11266  letr  11268  mul32  11340  mul31  11341  add32  11393  subsub23  11426  addsubass  11431  subcan2  11447  subsub2  11450  nppcan2  11453  sub32  11456  nnncan  11457  nnncan2  11459  pnpcan2  11462  subdi  11611  subdir  11612  receu  11823  mulcan1g  11831  mulcan2g  11832  divmul3  11842  divrec  11853  divrec2  11854  div11  11865  divsubdir  11876  subdivcomb2  11878  divdiv1  11893  redivcl  11901  div2neg  11905  ltmul2  12033  lemul1  12034  lemul2  12035  lemul2a  12037  lediv1  12048  gt0div  12049  ge0div  12050  mulsuble0b  12055  ltdivmul  12058  ledivmul  12059  ltdivmul2  12060  ledivmul2  12062  lemuldiv  12063  ltdiv23  12074  lediv23  12075  ledivp1i  12108  ltdivp1i  12109  uzind2  12627  nn0ind  12629  fnn0ind  12633  uz3m2nn  12853  xrltletr  13117  xrletr  13118  xrre2  13130  xrltmin  13142  xrlemin  13144  xleadd2a  13214  xleadd1  13215  xltadd2  13217  xmulasslem3  13246  xmulass  13247  xltmul2  13253  ixxdisj  13321  iooneg  13432  iccneg  13433  icoshft  13434  icoshftf1o  13435  icodisj  13437  snunioo  13439  fzen  13502  ssfzunsnext  13530  fzrev3  13551  2ffzeq  13610  fzoaddel2  13681  elfzodifsumelfzo  13692  ssfzoulel  13721  ssfzo12bi  13722  fzoopth  13723  fzoshftral  13745  adddivflid  13780  flltdivnn0lt  13795  ltdifltdiv  13796  fldiv4p1lem1div2  13797  modcyc  13868  modcyc2  13869  modaddabs  13873  muladdmod  13877  modsubmodmod  13895  modaddmodup  13899  modaddmulmod  13903  moddi  13904  modsubdir  13905  expdiv  14078  digit2  14201  nfile  14324  hashdifpr  14380  hashgt23el  14389  hashreshashfun  14404  hashf1dmcdm  14409  hash3tpexb  14459  fi1uzind  14472  ccatval1  14542  ccatass  14553  swrdval  14608  swrdnd  14619  swrd0  14623  swrdfv2  14626  pfxsuff1eqwrdeq  14664  swrdswrdlem  14669  pfxccatin12lem2a  14692  pfxccatin12lem1  14693  repswccat  14751  cshwidxmod  14768  cshwidxmodr  14769  cshf1  14775  repswcshw  14777  2cshw  14778  2cshwcom  14781  2cshwcshw  14791  cshwcsh2id  14794  ccatco  14801  2swrd2eqwrdeq  14919  wwlktovf  14922  brcnvtrclfv  14969  shftval2  15041  mulre  15087  absdiv  15261  absdiflt  15284  absdifle  15285  abs3dif  15298  cau3  15322  ello12r  15483  elo12r  15494  modfsummods  15759  geoisum1c  15846  rpnnen2lem4  16185  rpnnen2lem7  16188  addmulmodb  16235  dvdsmulc  16253  dvdsmulcr  16255  dvdsmultr1  16266  dvdsmultr2  16268  dvdssub2  16271  oexpneg  16315  divalgb  16374  ndvdsadd  16380  sadass  16441  modgcd  16502  dvdsgcd  16514  dvdsgcdb  16515  gcdass  16517  mulgcd  16518  absmulgcd  16519  rpmulgcd  16527  expgcd  16533  zexpgcd  16535  nn0seqcvgd  16540  algcvga  16549  lcmdvdsb  16583  lcmass  16584  lcmfunsnlem1  16607  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  coprmdvds  16623  coprmdvds2  16624  rpmul  16629  cncongr1  16637  cncongr2  16638  qnumdenbi  16714  modprm0  16776  coprimeprodsq  16779  pythagtriplem4  16790  pythagtriplem8  16794  pythagtriplem9  16795  pythagtriplem12  16797  pythagtriplem14  16799  pythagtriplem16  16801  pcpremul  16814  pcgcd  16849  vdwapval  16944  vdwapun  16945  prmgaplem3  17024  prmgaplem4  17025  prmgaplem7  17028  prmgapprmolem  17032  mreiincl  17557  mreincl  17560  mremre  17565  mrcss  17577  catcisolem  18072  pleval2  18296  pospo  18304  latlem  18396  latjcom  18406  latmcom  18422  lubss  18472  lubun  18474  clatglbss  18478  ipole  18493  ipolt  18494  pslem  18531  dirtr  18561  gsumsgrpccat  18767  gsumws2  18769  frmdmnd  18786  symggrplem  18811  isgrpi  18891  grpsubrcan  18953  grpinvsub  18954  grpsubeq0  18958  grpsubadd0sub  18959  grpnpcan  18964  qussub  19123  ghmsub  19156  symgpssefmnd  19326  symggrp  19330  symgextsymg  19354  gsmsymgreqlem2  19361  symgfixfolem1  19368  pmtrprfv3  19384  symggen  19400  lsmass  19599  efgsrel  19664  cntzcmn  19770  dvrcl  20313  unitdvcl  20314  dvrcan1  20318  subrngmre  20471  subrgmre  20506  rhmsubclem2  20595  rrgeq0  20609  abvsubtri  20736  abvtrivd  20741  lmodvsubval2  20823  rmodislmodlem  20835  rmodislmod  20836  lss0cl  20853  lssintcl  20870  lssincl  20871  reslmhm2  20960  lspvadd  21003  lspsntrim  21005  islbs3  21065  rnglidlmmgm  21155  cncrng  21300  cncrngOLD  21301  xrsmcmn  21303  cndrng  21310  cndrngOLD  21311  cnsrng  21317  xrs1mnd  21321  absabv  21341  psgnco  21492  zrhpsgninv  21494  zrhpsgnevpm  21500  zrhpsgnodpm  21501  zrhpsgnelbas  21503  zrhcopsgnelbas  21504  uvcresum  21702  lindfmm  21736  lindsmm  21737  evlsval2  21994  mamudm  22282  mamufacex  22283  matsubgcell  22321  matsc  22337  scmatscmide  22394  scmatrhmcl  22415  1marepvsma1  22470  m1detdiag  22484  mdetralt  22495  m2detleiblem7  22514  gsummatr01lem3  22544  gsummatr01  22546  smadiadetlem0  22548  decpmate  22653  decpmatcl  22654  pm2mpcl  22684  pm2mpghmlem2  22699  chfacfscmul0  22745  chfacfscmulgsum  22747  chfacfpmmul0  22749  chfacfpmmulgsum  22751  unopn  22790  clsss  22941  cldmre  22965  toponmre  22980  opnssneib  23002  restabs  23052  restcls  23068  restntr  23069  hausnei2  23240  cmpsublem  23286  bwth  23297  hausmapdom  23387  ptpjcn  23498  upxp  23510  ptrescn  23526  xkopjcn  23543  fbssfi  23724  snfil  23751  ufprim  23796  rnelfm  23840  flimrest  23870  fclsrest  23911  tmdgsum  23982  blpnfctr  24324  mscl  24349  xmscl  24350  xmsge0  24351  xmseq0  24352  restmetu  24458  ngpds  24492  tngngp3  24544  unitnmn0  24556  xrsxmet  24698  metds0  24739  mpomulcn  24758  cncfmptc  24805  isclmp  24997  cnlmod  25040  ncvsi  25051  cphsqrtcl  25084  cfil3i  25169  cfilres  25196  cmssmscld  25250  cmmbl  25435  voliunlem2  25452  itg2ub  25634  itgrecl  25699  r1pid  26066  eflogeq  26511  cxpadd  26588  cxpcom  26648  logbchbase  26681  relogbreexp  26685  relogbzexp  26686  relogbmulexp  26688  logbleb  26693  logblt  26694  lawcos  26726  pythag  26727  asinsinb  26807  acoscosb  26808  atantanb  26834  amgmlem  26900  lgsneg  27232  lgsne0  27246  lgsmodeq  27253  lgsmulsqcoprm  27254  gausslemma2dlem1a  27276  2sqreulem2  27363  sltres  27574  noetainflem1  27649  sltletr  27668  sletr  27670  nocvxmin  27690  madebdaylemold  27809  lrrecpo  27848  sltadd2im  27893  sleadd1im  27894  sleadd2im  27895  sleadd1  27896  sleadd2  27897  sltadd1  27899  addscan2  27900  addscan1  27901  subadds  27974  sltsub1  27980  divscl  28125  onscutlt  28165  expscllem  28316  0reno  28348  brbtwn2  28832  colinearalg  28837  eleesubd  28839  axcgrrflx  28841  axcgrtr  28842  axsegcon  28854  ax5seglem1  28855  ax5seglem2  28856  ax5seglem4  28859  axbtwnid  28866  axlowdimlem14  28882  axlowdim  28888  axcontlem5  28895  axcontlem7  28897  nb3grprlem2  29308  cplgr3v  29362  cusgrsizeindslem  29379  sizusglecusglem2  29390  umgr2v2e  29453  cusgrrusgr  29509  iswlk  29538  edginwlk  29563  uspgr2wlkeq  29574  uspgr2wlkeq2  29575  uspgr2wlkeqi  29576  wlkonprop  29586  wlkon2n0  29594  pthdadjvtx  29658  upgr2pthnlp  29662  spthonepeq  29682  pthdlem2lem  29697  crctcshwlkn0lem3  29742  crctcshwlkn0lem5  29744  wlkiswwlks2lem4  29802  wlkiswwlks2lem6  29804  wlklnwwlkln2lem  29812  wwlksnred  29822  wwlksnextbi  29824  wwlksnextwrd  29827  2pthdlem1  29860  2wlkdlem10  29865  umgr2adedgwlkonALT  29877  elwwlks2s3  29881  elwwlks2ons3im  29884  s3wwlks2on  29886  2wspdisj  29892  2wspiundisj  29893  clwwlkgt0  29915  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwlkclwwlk  29931  clwlkclwwlk2  29932  clwlkclwwlkfo  29938  clwwisshclwwslemlem  29942  erclwwlktr  29951  clwwlkf  29976  wwlksubclwwlk  29987  erclwwlkntr  30000  clwwlknon  30019  frcond1  30195  frgr3v  30204  3vfriswmgr  30207  frgrwopreglem4a  30239  frrusgrord0lem  30268  clwwnonrepclwwnon  30274  extwwlkfab  30281  numclwwlk1lem2f1  30286  numclwwlk1lem2fo  30287  clwlknon2num  30297  numclwwlk2lem1  30305  numclwlk2lem2f  30306  numclwlk2lem2f1o  30308  numclwwlk2  30310  frgrreggt1  30322  friendshipgt3  30327  imsmetlem  30619  nmoxr  30695  nmoolb  30700  blometi  30732  phpar2  30752  phpar  30753  ipasslem5  30764  hvadd32  30963  hvaddsub12  30967  hvaddsubass  30970  hvsubass  30973  hvsub32  30974  hvsubdistr1  30978  hvsubdistr2  30979  hvmulcan  31001  hvmulcan2  31002  hvsubcan  31003  his5  31015  his2sub  31021  hhssabloilem  31190  hhssnv  31193  shlej2  31290  pjoi0  31646  hodcl  31676  hoadd32  31712  hosubdi  31737  hosubsub2  31741  hoaddsubass  31744  hosubsub4  31747  nmoplb  31836  unop  31844  hmop  31851  nmfnlb  31853  lnopmul  31896  kbass1  32045  kbass2  32046  leopmul2i  32064  leoptr  32066  cvntr  32221  mdslmd4i  32262  mdexchi  32264  atcv1  32309  sumdmdii  32344  fcoinvbr  32534  fpwrelmapffs  32657  xreceu  32842  isinftm  33135  unitdivcld  33891  esummulc1  34071  hasheuni  34075  unelsiga  34124  inelpisys  34144  carsgsigalem  34306  signswmnd  34548  bnj545  34885  bnj594  34902  bnj1311  35014  fineqvac  35087  usgrgt2cycl  35117  subgrwlk  35119  acycgr1v  35136  cvmsf1o  35259  cvmscld  35260  satefvfmla1  35412  elnanelprv  35416  lediv2aALT  35664  gcd32  35736  fununiq  35756  dfrdg4  35939  brcolinear  36047  colinearex  36048  nn0prpwlem  36310  clsun  36316  fnemeet1  36354  fnemeet2  36355  fnejoin1  36356  fnejoin2  36357  eltail  36362  rdgeqoa  37358  nlpineqsn  37396  curf  37592  lindsadd  37607  poimirlem28  37642  cnambfre  37662  ftc1anclem4  37690  cocanfo  37713  f1ocan1fv  37720  metf1o  37749  ismtybnd  37801  ghomco  37885  isdrngo2  37952  inidl  38024  igenmin  38058  brxrn  38356  brredunds  38617  cmtvalN  39204  cvrval  39262  pmapmeet  39767  paddval  39792  paddssat  39808  elpcliN  39887  pclssN  39888  pclunN  39892  paddunN  39921  poldmj1N  39922  tendoplcl2  40772  tendoplcl  40775  dihmeet  41337  lcmineqlem1  42017  reltsub1  42374  reltsubadd2  42375  resubsub4  42377  reppncan  42381  resubdi  42384  readdcan2  42401  subresre  42419  mapco2g  42702  mzpcompact2lem  42739  eqrabdioph  42765  lerabdioph  42793  eluzrabdioph  42794  ltrabdioph  42796  nerabdioph  42797  dvdsrabdioph  42798  reglogcl  42878  rmxyadd  42910  rmyabs  42947  congadd  42955  congabseq  42963  rmydioph  43003  mendring  43177  mendlmod  43178  iocinico  43201  omge1  43286  relexp0a  43705  relexpaddss  43707  brcoffn  44019  ismnushort  44290  dvconstbi  44323  uzwo4  45047  ssin0  45049  ssinc  45081  ssdec  45082  fvmpt2bd  45164  disjf1o  45185  ssnnf1octb  45188  sub31  45288  fperiodmullem  45301  ssfiunibd  45307  infxr  45363  fmul01  45578  islptre  45617  lptre2pt  45638  limcleqr  45642  limclner  45649  limsuppnflem  45708  limsupvaluz2  45736  supcnvlimsup  45738  xlimmnfvlem2  45831  xlimmnfv  45832  xlimpnfvlem2  45835  xlimpnfv  45836  climxlim2lem  45843  coskpi2  45864  cosknegpi  45867  dvnmptdivc  45936  dvdsn1add  45937  dvnmptconst  45939  dvmptfprod  45943  dvnprodlem1  45944  dvnprodlem2  45945  ovolsplit  45986  stoweidlem60  46058  stowei  46062  dirkeritg  46100  fourierdlem70  46174  fourierdlem71  46175  fourierdlem103  46207  fourierdlem104  46208  fouriersw  46229  rrxtopnfi  46285  saluncl  46315  salexct  46332  sge0ltfirp  46398  sge0iunmpt  46416  meadjiunlem  46463  meaiuninc3v  46482  carageniuncllem1  46519  caratheodorylem1  46524  ovncvrrp  46562  ovnsubaddlem1  46568  hspmbllem2  46625  ovolval5lem3  46652  smfpimbor1lem1  46796  smfsuplem1  46809  smflimsuplem4  46821  sigarls  46855  cnambpcma  47295  elfzelfzlble  47322  submodaddmod  47342  difltmodne  47343  m1mod0mod1  47355  modmkpkne  47362  mod2addne  47365  modm2nep1  47367  modm1nep2  47369  modm1nem2  47370  fsumsplitsndif  47374  fundcmpsurinjALT  47413  iccpartiltu  47423  prproropf1olem2  47505  fmtno4prmfac  47573  2pwp1prmfmtno  47591  lighneallem4b  47610  mogoldbblem  47721  gbegt5  47762  sbgoldbm  47785  nnsum3primesle9  47795  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  evengpoap3  47800  nnsum4primesevenALTV  47802  clnbgredg  47840  opstrgric  47926  clnbgrgrimlem  47933  grtrif1o  47941  isubgr3stgrlem1  47965  isubgr3stgrlem4  47968  gpgusgralem  48047  gpg3nbgrvtx0  48067  isupwlk  48124  lidldomnnring  48224  2zrngacmnd  48236  rhmsubcALTVlem2  48270  fprmappr  48333  zlmodzxzscm  48345  gsumlsscl  48368  lincvalsng  48405  lincvalpr  48407  lincdifsn  48413  linc1  48414  lincellss  48415  fdivmpt  48529  digexp  48596  2arymaptfo  48643  line  48721  rrxline  48723  itsclc0xyqsolr  48758  iscnrm3r  48936  resipos  48963  amgmwlem  49791