Theorem 3adant1 1126

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3ad2ant2  1130  3ad2ant3  1131  3simpc  1146  eupickb  2720  spc3egv  3606  sbciegft  3810  reuhyp  5323  funopg  6391  funprg  6410  funtpg  6411  funcnvtp  6419  unima  6741  fvun1  6756  fnreseql  6820  xpprsng  6904  ftpg  6920  f13dfv  7033  mpoeq3ia  7234  ordunel  7544  fex2  7640  funexw  7655  poxp  7824  suppval1  7838  wfr3g  7955  smores3  7992  oaord  8175  oacan  8176  oaword  8177  omord  8196  omcan  8197  omwordri  8200  odi  8207  omass  8208  oeord  8216  oecan  8217  oewordri  8220  oeordsuc  8222  nnaord  8247  nnaordr  8248  nndi  8251  nnmass  8252  nnaword  8255  nnmord  8260  nnmwordri  8264  erov  8396  ecopovtrn  8402  ixpf  8486  mapxpen  8685  fimax2g  8766  unbnn  8776  funisfsupp  8840  inelfi  8884  elfiun  8896  sup0  8932  suppr  8937  infpr  8969  r111  9206  dif1card  9438  ackbij1lem16  9659  cff1  9682  cfflb  9683  cfsmolem  9694  fin23lem34  9770  hsmexlem2  9851  axcc3  9862  domtriomlem  9866  axdc3lem4  9877  axdc4lem  9879  axcclem  9881  konigthlem  9992  gchdomtri  10053  tskpr  10194  tskop  10195  tskuni  10207  tskun  10210  gruop  10229  gruun  10230  grudomon  10241  adderpqlem  10378  mulerpqlem  10379  addassnq  10382  mulassnq  10383  distrnq  10385  ltsonq  10393  ltanq  10395  ltmnq  10396  genpass  10433  distrlem1pr  10449  distrlem4pr  10450  ltsopr  10456  adddir  10634  axlttrn  10715  ltletr  10734  letr  10736  mul32  10808  mul31  10809  add32  10860  subsub23  10893  addsubass  10898  subcan2  10913  subsub2  10916  nppcan2  10919  sub32  10922  nnncan  10923  nnncan2  10925  pnpcan2  10928  subdi  11075  subdir  11076  receu  11287  mulcan1g  11295  mulcan2g  11296  divmul3  11305  divrec  11316  divrec2  11317  divsubdir  11336  subdivcomb2  11338  divdiv1  11353  redivcl  11361  div2neg  11365  ltmul2  11493  lemul1  11494  lemul2  11495  lemul2a  11497  lediv1  11507  gt0div  11508  ge0div  11509  mulsuble0b  11514  ltdivmul  11517  ledivmul  11518  ltdivmul2  11519  ledivmul2  11521  lemuldiv  11522  ltdiv23  11533  lediv23  11534  ledivp1i  11567  ltdivp1i  11568  uzind2  12078  nn0ind  12080  fnn0ind  12084  uz3m2nn  12294  xrltletr  12553  xrletr  12554  xrre2  12566  xrltmin  12578  xrlemin  12580  xleadd2a  12650  xleadd1  12651  xltadd2  12653  xmulasslem3  12682  xmulass  12683  xltmul2  12689  ixxdisj  12756  iooneg  12860  iccneg  12861  icoshft  12862  icoshftf1o  12863  icodisj  12865  snunioo  12867  fzen  12927  ssfzunsnext  12955  fzrev3  12976  2ffzeq  13031  fzoaddel2  13096  elfzodifsumelfzo  13106  ssfzoulel  13134  ssfzo12bi  13135  fzoshftral  13157  adddivflid  13191  flltdivnn0lt  13206  ltdifltdiv  13207  fldiv4p1lem1div2  13208  modcyc  13277  modcyc2  13278  modaddabs  13280  modsubmodmod  13301  modaddmodup  13305  modaddmulmod  13309  moddi  13310  modsubdir  13311  expdiv  13483  digit2  13600  nfile  13723  hashdifpr  13779  hashgt23el  13788  hashreshashfun  13803  fi1uzind  13858  ccatval1  13932  ccatass  13944  swrdval  14007  swrdnd  14018  swrd0  14022  swrdfv2  14025  pfxsuff1eqwrdeq  14063  swrdswrdlem  14068  pfxccatin12lem2a  14091  pfxccatin12lem1  14092  repswccat  14150  cshwidxmod  14167  cshwidxmodr  14168  cshf1  14174  repswcshw  14176  2cshw  14177  2cshwcom  14180  2cshwcshw  14189  cshwcsh2id  14192  ccatco  14199  2swrd2eqwrdeq  14317  wwlktovf  14322  brcnvtrclfv  14365  shftval2  14436  mulre  14482  absdiv  14657  absdiflt  14679  absdifle  14680  abs3dif  14693  cau3  14717  ello12r  14876  elo12r  14887  modfsummods  15150  geoisum1c  15238  rpnnen2lem4  15572  rpnnen2lem7  15575  dvdsmulc  15639  dvdsmulcr  15641  dvdsmultr1  15649  dvdsmultr2  15651  dvdssub2  15653  oexpneg  15696  divalgb  15757  ndvdsadd  15763  sadass  15822  modgcd  15882  dvdsgcd  15894  dvdsgcdb  15895  gcdass  15897  mulgcd  15898  absmulgcd  15899  rpmulgcd  15908  nn0seqcvgd  15916  algcvga  15925  lcmdvdsb  15959  lcmass  15960  lcmfunsnlem1  15983  lcmfunsnlem2lem1  15984  lcmfunsnlem2lem2  15985  coprmdvds  15999  coprmdvds2  16000  rpmul  16005  cncongr1  16013  cncongr2  16014  qnumdenbi  16086  modprm0  16144  coprimeprodsq  16147  pythagtriplem4  16158  pythagtriplem8  16162  pythagtriplem9  16163  pythagtriplem12  16165  pythagtriplem14  16167  pythagtriplem16  16169  pcpremul  16182  pcgcd  16216  vdwapval  16311  vdwapun  16312  prmgaplem3  16391  prmgaplem4  16392  prmgaplem7  16395  prmgapprmolem  16399  mreiincl  16869  mreincl  16872  mremre  16877  mrcss  16889  catcisolem  17368  pleval2  17577  pospo  17585  latlem  17661  latjcom  17671  latmcom  17687  lubss  17733  lubun  17735  clatglbss  17739  ipole  17770  ipolt  17771  pslem  17818  dirtr  17848  gsumsgrpccat  18006  gsumws2  18009  frmdmnd  18026  symggrplem  18051  isgrpi  18128  grpsubrcan  18182  grpinvsub  18183  grpsubeq0  18187  grpsubadd0sub  18188  grpnpcan  18193  qussub  18342  ghmsub  18368  symgpssefmnd  18526  symggrp  18530  symgextsymg  18554  gsmsymgreqlem2  18561  symgfixfolem1  18568  pmtrprfv3  18584  symggen  18600  lsmass  18797  efgsrel  18862  cntzcmn  18962  dvrcl  19438  unitdvcl  19439  dvrcan1  19443  subrgmre  19561  abvsubtri  19608  abvtrivd  19613  lmodvsubval2  19691  rmodislmodlem  19703  rmodislmod  19704  lss0cl  19720  lssintcl  19738  lssincl  19739  reslmhm2  19827  lspvadd  19870  lspsntrim  19872  islbs3  19929  rrgeq0  20065  evlsval2  20302  cncrng  20568  xrsmcmn  20570  cndrng  20576  cnsrng  20581  xrs1mnd  20585  absabv  20604  psgnco  20729  zrhpsgninv  20731  zrhpsgnevpm  20737  zrhpsgnodpm  20738  zrhpsgnelbas  20740  zrhcopsgnelbas  20741  uvcresum  20939  lindfmm  20973  lindsmm  20974  mamudm  21001  mamufacex  21002  matsubgcell  21045  matsc  21061  scmatscmide  21118  scmatrhmcl  21139  1marepvsma1  21194  m1detdiag  21208  mdetralt  21219  m2detleiblem7  21238  gsummatr01lem3  21268  gsummatr01  21270  smadiadetlem0  21272  decpmate  21376  decpmatcl  21377  pm2mpcl  21407  pm2mpghmlem2  21422  chfacfscmul0  21468  chfacfscmulgsum  21470  chfacfpmmul0  21472  chfacfpmmulgsum  21474  unopn  21513  clsss  21664  cldmre  21688  toponmre  21703  opnssneib  21725  restabs  21775  restcls  21791  restntr  21792  hausnei2  21963  cmpsublem  22009  bwth  22020  hausmapdom  22110  ptpjcn  22221  upxp  22233  ptrescn  22249  xkopjcn  22266  fbssfi  22447  snfil  22474  ufprim  22519  rnelfm  22563  flimrest  22593  fclsrest  22634  tmdgsum  22705  blpnfctr  23048  mscl  23073  xmscl  23074  xmsge0  23075  xmseq0  23076  restmetu  23182  ngpds  23215  tngngp3  23267  unitnmn0  23279  xrsxmet  23419  metds0  23460  cncfmptc  23521  isclmp  23703  cnlmod  23746  ncvsi  23757  cphsqrtcl  23790  cfil3i  23874  cfilres  23901  cmssmscld  23955  cmmbl  24137  voliunlem2  24154  itg2ub  24336  itgrecl  24400  tdeglem3  24655  r1pid  24755  eflogeq  25187  cxpadd  25264  cxpcom  25322  logbchbase  25351  relogbreexp  25355  relogbzexp  25356  relogbmulexp  25358  logbleb  25363  logblt  25364  lawcos  25396  pythag  25397  asinsinb  25477  acoscosb  25478  atantanb  25504  amgmlem  25569  lgsneg  25899  lgsne0  25913  lgsmodeq  25920  lgsmulsqcoprm  25921  gausslemma2dlem1a  25943  2sqreulem2  26030  brbtwn2  26693  colinearalg  26698  eleesubd  26700  axcgrrflx  26702  axcgrtr  26703  axsegcon  26715  ax5seglem1  26716  ax5seglem2  26717  ax5seglem4  26720  axbtwnid  26727  axlowdimlem14  26743  axlowdim  26749  axcontlem5  26756  axcontlem7  26758  nb3grprlem2  27165  cplgr3v  27219  cusgrsizeindslem  27235  sizusglecusglem2  27246  umgr2v2e  27309  cusgrrusgr  27365  iswlk  27394  edginwlk  27418  uspgr2wlkeq  27429  uspgr2wlkeq2  27430  uspgr2wlkeqi  27431  wlkonprop  27442  wlkon2n0  27450  pthdadjvtx  27513  upgr2pthnlp  27515  spthonepeq  27535  pthdlem2lem  27550  crctcshwlkn0lem3  27592  crctcshwlkn0lem5  27594  wlkiswwlks2lem4  27652  wlkiswwlks2lem6  27654  wlklnwwlkln2lem  27662  wwlksnred  27672  wwlksnextbi  27674  wwlksnextwrd  27677  2pthdlem1  27711  2wlkdlem10  27716  umgr2adedgwlkonALT  27728  elwwlks2s3  27732  elwwlks2ons3im  27735  s3wwlks2on  27737  2wspdisj  27743  2wspiundisj  27744  clwwlkgt0  27766  clwlkclwwlklem2a4  27777  clwlkclwwlklem2a  27778  clwlkclwwlk  27782  clwlkclwwlk2  27783  clwlkclwwlkfo  27789  clwwisshclwwslemlem  27793  erclwwlktr  27802  clwwlkf  27828  wwlksubclwwlk  27839  erclwwlkntr  27852  clwwlknon  27871  frcond1  28047  frgr3v  28056  3vfriswmgr  28059  frgrwopreglem4a  28091  frrusgrord0lem  28120  clwwnonrepclwwnon  28126  extwwlkfab  28133  numclwwlk1lem2f1  28138  numclwwlk1lem2fo  28139  clwlknon2num  28149  numclwwlk2lem1  28157  numclwlk2lem2f  28158  numclwlk2lem2f1o  28160  numclwwlk2  28162  frgrreggt1  28174  friendshipgt3  28179  imsmetlem  28469  nmoxr  28545  nmoolb  28550  blometi  28582  phpar2  28602  phpar  28603  ipasslem5  28614  hvadd32  28813  hvaddsub12  28817  hvaddsubass  28820  hvsubass  28823  hvsub32  28824  hvsubdistr1  28828  hvsubdistr2  28829  hvmulcan  28851  hvmulcan2  28852  hvsubcan  28853  his5  28865  his2sub  28871  hhssabloilem  29040  hhssnv  29043  shlej2  29140  pjoi0  29496  hodcl  29526  hoadd32  29562  hosubdi  29587  hosubsub2  29591  hoaddsubass  29594  hosubsub4  29597  nmoplb  29686  unop  29694  hmop  29701  nmfnlb  29703  lnopmul  29746  kbass1  29895  kbass2  29896  leopmul2i  29914  leoptr  29916  cvntr  30071  mdslmd4i  30112  mdexchi  30114  atcv1  30159  sumdmdii  30194  fcoinvbr  30360  fpwrelmapffs  30472  xreceu  30600  isinftm  30812  unitdivcld  31146  esummulc1  31342  hasheuni  31346  unelsiga  31395  inelpisys  31415  carsgsigalem  31575  signswmnd  31829  bnj545  32169  bnj594  32186  bnj1311  32298  hashf1dmcdm  32358  usgrgt2cycl  32379  subgrwlk  32381  acycgr1v  32398  cvmsf1o  32521  cvmscld  32522  satefvfmla1  32674  elnanelprv  32678  lediv2aALT  32922  gcd32  32985  fununiq  33014  trpredpo  33076  poseq  33097  frr3g  33123  sltres  33171  sltletr  33237  sletr  33239  nocvxmin  33250  dfrdg4  33414  brcolinear  33522  colinearex  33523  nn0prpwlem  33672  clsun  33678  fnemeet1  33716  fnemeet2  33717  fnejoin1  33718  fnejoin2  33719  eltail  33724  rdgeqoa  34653  nlpineqsn  34691  curf  34872  lindsadd  34887  poimirlem28  34922  cnambfre  34942  ftc1anclem4  34972  cocanfo  34995  f1ocan1fv  35003  metf1o  35032  ismtybnd  35087  ghomco  35171  isdrngo2  35238  inidl  35310  igenmin  35344  brxrn  35628  brredunds  35863  cmtvalN  36349  cvrval  36407  pmapmeet  36911  paddval  36936  paddssat  36952  elpcliN  37031  pclssN  37032  pclunN  37036  paddunN  37065  poldmj1N  37066  tendoplcl2  37916  tendoplcl  37919  dihmeet  38481  factwoffsmonot  39105  expgcd  39190  zexpgcd  39192  reltsub1  39223  reltsubadd2  39224  resubsub4  39226  reppncan  39230  resubdi  39233  readdcan2  39249  mapco2g  39318  mzpcompact2lem  39355  eqrabdioph  39381  lerabdioph  39409  eluzrabdioph  39410  ltrabdioph  39412  nerabdioph  39413  dvdsrabdioph  39414  reglogcl  39494  rmxyadd  39525  rmyabs  39562  congadd  39570  congabseq  39578  rmydioph  39618  mendring  39799  mendlmod  39800  iocinico  39825  relexp0a  40068  relexpaddss  40070  brcoffn  40387  dvconstbi  40673  uzwo4  41322  ssin0  41324  ssinc  41360  ssdec  41361  fvmpt2bd  41433  disjf1o  41459  ssnnf1octb  41463  sub31  41564  fperiodmullem  41577  ssfiunibd  41583  infxr  41642  fmul01  41868  islptre  41907  lptre2pt  41928  limcleqr  41932  limclner  41939  limsuppnflem  41998  limsupvaluz2  42026  supcnvlimsup  42028  xlimmnfvlem2  42121  xlimmnfv  42122  xlimpnfvlem2  42125  xlimpnfv  42126  climxlim2lem  42133  coskpi2  42154  cosknegpi  42157  dvnmptdivc  42230  dvdsn1add  42231  dvnmptconst  42233  dvmptfprod  42237  dvnprodlem1  42238  dvnprodlem2  42239  ovolsplit  42280  stoweidlem60  42352  stowei  42356  dirkeritg  42394  fourierdlem70  42468  fourierdlem71  42469  fourierdlem103  42501  fourierdlem104  42502  fouriersw  42523  rrxtopnfi  42579  saluncl  42609  salexct  42624  sge0ltfirp  42689  sge0iunmpt  42707  meadjiunlem  42754  meaiuninc3v  42773  carageniuncllem1  42810  caratheodorylem1  42815  ovncvrrp  42853  ovnsubaddlem1  42859  hspmbllem2  42916  ovolval5lem3  42943  smfpimbor1lem1  43080  smfsuplem1  43092  smflimsuplem4  43104  sigarls  43121  cnambpcma  43501  elfzelfzlble  43528  fzoopth  43534  m1mod0mod1  43536  fsumsplitsndif  43540  fundcmpsurinjALT  43579  iccpartiltu  43589  prproropf1olem2  43673  fmtno4prmfac  43741  2pwp1prmfmtno  43759  lighneallem4b  43781  mogoldbblem  43892  gbegt5  43933  sbgoldbm  43956  nnsum3primesle9  43966  nnsum4primesodd  43968  nnsum4primesoddALTV  43969  evengpoap3  43971  nnsum4primesevenALTV  43973  isomgrtr  44011  strisomgrop  44012  isupwlk  44018  lidldomnnring  44208  2zrngacmnd  44220  rhmsubclem2  44365  rhmsubcALTVlem2  44383  zlmodzxzscm  44412  gsumlsscl  44438  lincvalsng  44478  lincvalpr  44480  lincdifsn  44486  linc1  44487  lincellss  44488  difmodm1lt  44589  fdivmpt  44607  digexp  44674  line  44726  rrxline  44728  itsclc0xyqsolr  44763  amgmwlem  44910