MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3adant1 Structured version   Visualization version   GIF version

Theorem 3adant1 1071
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
Hypothesis
Ref Expression
3adant.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
3adant1 ((𝜃𝜑𝜓) → 𝜒)

Proof of Theorem 3adant1
StepHypRef Expression
1 3simpc 1052 . 2 ((𝜃𝜑𝜓) → (𝜑𝜓))
2 3adant.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl 17 1 ((𝜃𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  3ad2ant2  1075  3ad2ant3  1076  eupickb  2525  sbciegft  3432  reuhyp  4816  funopg  5821  funprg  5839  funtpg  5841  funcnvtp  5850  fvun1  6163  fnreseql  6219  ftpg  6305  f13dfv  6407  mpt2eq3ia  6595  ordunel  6896  fex2  6991  poxp  7153  suppval1  7165  wfr3g  7277  smores3  7314  oaord  7491  oacan  7492  oaword  7493  omord  7512  omcan  7513  omwordri  7516  odi  7523  omass  7524  oeord  7532  oecan  7533  oewordri  7536  oeordsuc  7538  nnaord  7563  nnaordr  7564  nndi  7567  nnmass  7568  nnaword  7571  nnmord  7576  nnmwordri  7580  erov  7708  ecopovtrn  7714  ixpf  7793  mapxpen  7988  fimax2g  8068  unbnn  8078  funisfsupp  8140  inelfi  8184  elfiun  8196  sup0  8232  suppr  8237  infpr  8269  r111  8498  dif1card  8693  xpcdaen  8865  mapcdaen  8866  ackbij1lem16  8917  cff1  8940  cfflb  8941  cfsmolem  8952  fin23lem34  9028  hsmexlem2  9109  axcc3  9120  domtriomlem  9124  axdc3lem4  9135  axdc4lem  9137  axcclem  9139  konigthlem  9246  gchdomtri  9307  tskpr  9448  tskop  9449  tskuni  9461  tskun  9464  gruop  9483  gruun  9484  grudomon  9495  adderpqlem  9632  mulerpqlem  9633  addassnq  9636  mulassnq  9637  distrnq  9639  ltsonq  9647  ltanq  9649  ltmnq  9650  genpass  9687  distrlem1pr  9703  distrlem4pr  9704  ltsopr  9710  adddir  9887  axlttrn  9961  ltletr  9980  letr  9982  mul32  10054  mul31  10055  add32  10105  subsub23  10137  addsubass  10142  subcan2  10157  subsub2  10160  nppcan2  10163  sub32  10166  nnncan  10167  nnncan2  10169  pnpcan2  10172  subdi  10314  subdir  10315  receu  10523  mulcan1g  10531  mulcan2g  10532  divmul3  10541  divrec  10552  divrec2  10553  divsubdir  10572  divdiv1  10587  redivcl  10595  div2neg  10599  ltmul2  10725  lemul1  10726  lemul2  10727  lemul2a  10729  lediv1  10739  gt0div  10740  ge0div  10741  mulsuble0b  10746  ltdivmul  10749  ledivmul  10750  ltdivmul2  10751  ledivmul2  10753  lemuldiv  10754  ltdiv23  10765  lediv23  10766  ledivp1i  10800  ltdivp1i  10801  uzind2  11304  nn0ind  11306  fnn0ind  11310  uz3m2nn  11565  xrltletr  11825  xrletr  11826  xrre2  11836  xrltmin  11848  xrlemin  11850  xleadd2a  11915  xleadd1  11916  xltadd2  11918  xmulasslem3  11947  xmulass  11948  xltmul2  11954  ixxdisj  12019  iooneg  12121  iccneg  12122  icoshft  12123  icoshftf1o  12124  icodisj  12126  snunioo  12127  fzen  12186  ssfzunsn  12214  fzrev3  12233  2ffzeq  12286  fzoaddel2  12348  elfzodifsumelfzo  12358  ssfzoulel  12385  ssfzo12bi  12386  fzoshftral  12404  adddivflid  12438  flltdivnn0lt  12453  ltdifltdiv  12454  fldiv4p1lem1div2  12455  modcyc  12524  modcyc2  12525  modaddabs  12527  modsubmodmod  12548  modaddmodup  12552  modaddmulmod  12556  moddi  12557  modsubdir  12558  expdiv  12730  digit2  12816  hashdifpr  13018  fi1uzind  13082  fi1uzindOLD  13088  ccatass  13172  lswccatn0lsw  13174  swrdval  13217  swrdnd  13232  swrd0  13234  swrdfv2  13246  2swrd1eqwrdeq  13254  swrdswrdlem  13259  swrdccatin12lem2a  13284  swrdccatin12lem2b  13285  repswccat  13331  cshwidxmod  13348  cshwidxmodr  13349  cshf1  13355  repswcshw  13357  2cshw  13358  2cshwcom  13361  2cshwcshw  13370  cshwcsh2id  13373  ccatco  13380  2swrd2eqwrdeq  13492  wwlktovf  13495  brcnvtrclfv  13540  shftval2  13611  mulre  13657  absdiv  13831  absdiflt  13853  absdifle  13854  abs3dif  13867  cau3  13891  ello12r  14044  elo12r  14055  modfsummods  14314  geoisum1c  14398  rpnnen2lem4  14733  rpnnen2lem7  14736  dvdsmulc  14795  dvdsmulcr  14797  dvdsmultr1  14805  dvdsmultr2  14807  dvdssub2  14809  oexpneg  14855  divalgb  14913  ndvdsadd  14920  sadass  14979  modgcd  15039  dvdsgcd  15047  dvdsgcdb  15048  gcdass  15050  mulgcd  15051  absmulgcd  15052  rpmulgcd  15061  nn0seqcvgd  15069  algcvga  15078  lcmdvdsb  15112  lcmass  15113  lcmfunsnlem1  15136  lcmfunsnlem2lem1  15137  lcmfunsnlem2lem2  15138  coprmdvds  15152  coprmdvdsOLD  15153  coprmdvds2  15154  rpmul  15159  cncongr1  15167  cncongr2  15168  prmgt1  15195  qnumdenbi  15238  modprm0  15296  coprimeprodsq  15299  pythagtriplem4  15310  pythagtriplem8  15314  pythagtriplem9  15315  pythagtriplem12  15317  pythagtriplem14  15319  pythagtriplem16  15321  pcpremul  15334  pcgcd  15368  vdwapval  15463  vdwapun  15464  prmgaplem3  15543  prmgaplem4  15544  prmgaplem7  15547  prmgapprmolem  15551  setsstruct  15675  mreiincl  16027  mreincl  16030  mremre  16035  mrcss  16047  catcisolem  16527  pleval2  16736  pospo  16744  latlem  16820  latjcom  16830  latmcom  16846  lubss  16892  lubun  16894  clatglbss  16898  ipole  16929  ipolt  16930  pslem  16977  dirtr  17007  gsumws2  17150  frmdmnd  17167  isgrpi  17216  grpsubrcan  17267  grpinvsub  17268  grpsubeq0  17272  grpsubadd0sub  17273  grpnpcan  17278  qussub  17425  ghmsub  17439  symggrp  17591  symgextsymg  17615  gsmsymgreqlem2  17622  symgfixfolem1  17629  pmtrprfv3  17645  symggen  17661  lsmass  17854  efgsrel  17918  cntzcmn  18016  dvrcl  18457  unitdvcl  18458  dvrcan1  18462  subrgmre  18575  abvsubtri  18606  abvtrivd  18611  lmodvsubval2  18689  lss0cl  18716  lssintcl  18733  lssincl  18734  reslmhm2  18822  lspvadd  18865  lspsntrim  18867  islbs3  18924  rrgeq0  19059  evlsval2  19289  cncrng  19534  xrsmcmn  19536  cndrng  19542  cnsrng  19547  xrs1mnd  19551  absabv  19570  psgnco  19695  zrhpsgninv  19697  zrhpsgnevpm  19703  zrhpsgnodpm  19704  zrhpsgnelbas  19706  zrhcopsgnelbas  19707  uvcresum  19898  lindfmm  19932  lindsmm  19933  mamudm  19960  mamufacex  19961  matsubgcell  20006  matsc  20022  scmatscmide  20079  scmatrhmcl  20100  1marepvsma1  20155  m1detdiag  20169  mdetralt  20180  m2detleiblem7  20199  gsummatr01lem3  20229  gsummatr01  20231  smadiadetlem0  20233  decpmate  20337  decpmatcl  20338  pm2mpcl  20368  pm2mpghmlem2  20383  chfacfscmul0  20429  chfacfscmulgsum  20431  chfacfpmmul0  20433  chfacfpmmulgsum  20435  unopn  20480  clsss  20615  cldmre  20639  toponmre  20654  opnssneib  20676  restabs  20726  restcls  20742  restntr  20743  hausnei2  20914  cmpsublem  20959  bwth  20970  hausmapdom  21060  ptpjcn  21171  upxp  21183  ptrescn  21199  xkopjcn  21216  fbssfi  21398  snfil  21425  ufprim  21470  rnelfm  21514  flimrest  21544  fclsrest  21585  tmdgsum  21656  blpnfctr  21998  mscl  22023  xmscl  22024  xmsge0  22025  xmseq0  22026  restmetu  22132  ngpds  22165  tngngp3  22217  unitnmn0  22229  xrsxmet  22367  metds0  22408  cncfmptc  22469  isclmp  22652  cnlmod  22695  ncvsi  22703  cphsqrtcl  22736  cfil3i  22819  cfilres  22846  cmmbl  23053  voliunlem2  23070  itg2ub  23250  itgrecl  23314  tdeglem3  23567  r1pid  23667  eflogeq  24096  cxpadd  24169  logbchbase  24253  relogbreexp  24257  relogbzexp  24258  relogbmulexp  24260  logbleb  24265  logblt  24266  lawcos  24290  pythag  24291  asinsinb  24368  acoscosb  24369  atantanb  24395  amgmlem  24460  lgsneg  24790  lgsne0  24804  lgsmodeq  24811  lgsmulsqcoprm  24812  gausslemma2dlem1a  24834  brbtwn2  25530  colinearalg  25535  eleesubd  25537  axcgrrflx  25539  axcgrtr  25540  axsegcon  25552  ax5seglem1  25553  ax5seglem2  25554  ax5seglem4  25557  axbtwnid  25564  axlowdimlem14  25580  axlowdim  25586  axcontlem5  25593  axcontlem7  25595  nb3graprlem2  25774  cusgra3v  25786  cusgrasizeindslem2  25796  sizeusglecusglem2  25806  iswlkg  25845  edgwlk  25852  usgrwlknloop  25886  spthonepeq  25910  constr2spth  25923  constr2pth  25924  redwlk  25929  usgra2adedgwlkonALT  25937  cyclispthon  25954  usgrcyclnl1  25961  usgrcyclnl2  25962  3v3e3cycl1  25965  constr3lem5  25969  constr3trllem2  25972  constr3pthlem2  25977  4cycl4v4e  25987  4cycl4dv4e  25989  wwlknimp  26008  wlkiswwlk1  26011  wlkiswwlk2lem4  26015  wlkiswwlk2lem6  26017  usg2wlkeq  26029  usg2wlkeq2  26030  wlkiswwlkinj  26039  wlkiswwlksur  26040  wwlknred  26044  wwlknextbi  26046  isclwlkg  26076  clwlkisclwwlklem2a1  26100  clwlkisclwwlklem2a4  26105  clwlkisclwwlklem2a  26106  clwlkisclwwlk  26110  clwlkisclwwlk2  26111  clwwlkf  26115  wwlksubclwwlk  26125  clwwisshclwwlem1  26126  erclwwlktr  26136  eleclclwwlknlem1  26138  usg2cwwkdifex  26142  erclwwlkntr  26148  hashecclwwlkn1  26154  usghashecclwwlk  26155  hashclwwlkn  26156  clwlkfclwwlk  26164  el2spthonot  26190  el2spthonot0  26191  usg2wlkonot  26203  vdgrfval  26215  rusgrargra  26250  rusgranumwlklem4  26272  frgra3v  26322  3vfriswmgra  26325  frgrawopreg  26369  frg2woteu  26375  frgregordn0  26390  extwwlkfablem2lem  26395  numclwwlkovfel2  26403  numclwwlkovf2ex  26406  numclwwlkovgelim  26409  extwwlkfab  26410  numclwlk1lem2f1  26414  numclwlk1lem2fo  26415  numclwwlk2lem1  26422  numclwlk2lem2f  26423  numclwlk2lem2f1o  26425  frgrareggt1  26436  frgrareg  26437  frgraregord013  26438  friendshipgt3  26441  imsmetlem  26722  nmoxr  26798  nmoolb  26803  blometi  26835  phpar2  26855  phpar  26856  ipasslem5  26867  hvadd32  27068  hvaddsub12  27072  hvaddsubass  27075  hvsubass  27078  hvsub32  27079  hvsubdistr1  27083  hvsubdistr2  27084  hvmulcan  27106  hvmulcan2  27107  hvsubcan  27108  his5  27120  his2sub  27126  hhssabloilem  27295  hhssnv  27298  shlej2  27397  pjoi0  27753  hodcl  27783  hoadd32  27819  hosubdi  27844  hosubsub2  27848  hoaddsubass  27851  hosubsub4  27854  nmoplb  27943  unop  27951  hmop  27958  nmfnlb  27960  lnopmul  28003  kbass1  28152  kbass2  28153  leopmul2i  28171  leoptr  28173  cvntr  28328  mdslmd4i  28369  mdexchi  28371  atcv1  28416  sumdmdii  28451  fcoinvbr  28592  fpwrelmapffs  28690  xreceu  28754  isinftm  28859  unitdivcld  29068  esummulc1  29263  hasheuni  29267  unelsiga  29317  inelpisys  29337  carsgsigalem  29497  signswmnd  29753  bnj545  30012  bnj594  30029  bnj1311  30139  cvmsf1o  30301  cvmscld  30302  lediv2aALT  30618  subdivcomb2  30658  gcd32  30683  fununiq  30706  trpredpo  30772  poseq  30787  frr3g  30816  sltres  30854  nocvxmin  30883  dfrdg4  31021  brcolinear  31129  colinearex  31130  nn0prpwlem  31280  clsun  31286  fnemeet1  31324  fnemeet2  31325  fnejoin1  31326  fnejoin2  31327  eltail  31332  rdgeqoa  32177  curf  32340  poimirlem28  32390  cnambfre  32411  ftc1anclem4  32441  cocanfo  32465  f1ocan1fv  32474  metf1o  32504  ismtybnd  32559  ghomco  32643  isdrngo2  32710  inidl  32782  igenmin  32816  cmtvalN  33299  cvrval  33357  pmapmeet  33860  paddval  33885  paddssat  33901  elpcliN  33980  pclssN  33981  pclunN  33985  paddunN  34014  poldmj1N  34015  tendoplcl2  34867  tendoplcl  34870  dihmeet  35433  mapco2g  36078  mzpcompact2lem  36115  eqrabdioph  36142  lerabdioph  36170  eluzrabdioph  36171  ltrabdioph  36173  nerabdioph  36174  dvdsrabdioph  36175  reglogcl  36255  rmxyadd  36287  rmyabs  36326  congadd  36334  congabseq  36342  rmydioph  36382  mendring  36564  mendlmod  36565  iocinico  36599  relexp0a  36810  relexpaddss  36812  brcoffn  37131  dvconstbi  37338  uzwo4  38029  ssinc  38075  ssdec  38076  unima  38123  fvmpt2bd  38128  disjf1o  38156  ssnnf1octb  38160  sub31  38227  fperiodmullem  38241  ssfiunibd  38247  infxr  38307  fmul01  38430  islptre  38469  lptre2pt  38490  limcleqr  38494  limclner  38501  coskpi2  38532  cosknegpi  38535  dvnmptdivc  38611  dvdsn1add  38612  dvnmptconst  38614  dvmptfprod  38618  dvnprodlem1  38619  dvnprodlem2  38620  ovolsplit  38664  stoweidlem60  38736  stowei  38740  dirkeritg  38778  fourierdlem70  38852  fourierdlem71  38853  fourierdlem103  38885  fourierdlem104  38886  fouriersw  38907  rrxtopnfi  38965  saluncl  38996  salexct  39011  sge0ltfirp  39076  sge0iunmpt  39094  meadjiunlem  39141  carageniuncllem1  39194  caratheodorylem1  39199  ovncvrrp  39237  ovnsubaddlem1  39243  hspmbllem2  39300  ovolval5lem3  39327  smfpimbor1lem1  39466  sigarls  39478  m1mod0mod1  39733  iccpartiltu  39744  fmtno4prmfac  39806  2pwp1prmfmtno  39826  lighneallem4b  39848  oexpnegALTV  39910  gbegt5  39967  nnsum3primesle9  39994  nnsum4primesodd  39996  nnsum4primesoddALTV  39997  evengpoap3  39999  nnsum4primesevenALTV  40001  pfxsuff1eqwrdeq  40054  ccatpfx  40056  pfx2  40059  pfxccatin12lem1  40070  cnambpcma  40147  elfzelfzlble  40164  fzoopth  40166  nfile  40175  fsumsplitsndif  40201  funvtxdmge2val  40228  funiedgdmge2val  40229  uhgruhgra  40273  uhgrauhgrbi  40275  usgr1v0e  40526  nb3grprlem2  40590  cplgr3v  40638  cusgrsizeindslem  40648  sizusglecusglem2  40659  umgr2v2e  40722  cusgrrusgr  40762  is1wlk  40794  isWlk  40795  uspgr2wlkeq  40835  uspgr2wlkeq2  40836  uspgr2wlkeqi  40837  wlkOn2n0  40855  pthdadjvtx  40917  upgr2pthnlp  40919  spthonepeq-av  40939  usgr2wlkspth  40946  pthdlem2lem  40954  uspgrn2crct  40992  crctcsh1wlkn0lem3  40996  crctcsh1wlkn0lem5  40998  1wlkiswwlks2lem4  41050  1wlkiswwlks2lem6  41052  1wlklnwwlkln2lem  41060  wwlksnred  41079  wwlksnextbi  41081  wwlksnextwrd  41084  2pthdlem1  41118  21wlkdlem10  41123  umgr2adedgwlkonALT  41135  elwwlks2ons3  41140  s3wwlks2on  41141  elwspths2on  41144  clwwlknp  41176  isclwwlksng  41177  clwlkclwwlklem2a4  41187  clwlkclwwlklem2a  41188  clwlkclwwlk  41192  clwlkclwwlk2  41193  clwwlksgt0  41194  clwwlksf  41203  wwlksubclwwlks  41213  clwwisshclwwslemlem  41214  erclwwlkstr  41224  erclwwlksntr  41236  clwlksfclwwlk  41250  upgreupthi  41357  frcond1  41419  frgr3v  41426  3vfriswmgr  41429  frgrwopreg  41467  frgr2wwlkeu  41473  frrusgrord0  41484  av-extwwlkfablem2lem  41488  av-numclwwlkffin  41493  av-numclwwlkovfel2  41495  av-numclwwlkovf2ex  41498  av-extwwlkfab  41501  av-numclwlk1lem2f1  41505  av-numclwlk1lem2fo  41506  av-numclwwlk2lem1  41513  av-numclwlk2lem2f  41514  av-numclwlk2lem2f1o  41516  av-numclwwlk2  41518  av-frgrareggt1  41528  av-friendshipgt3  41533  lidldomnnring  41701  2zrngacmnd  41713  rhmsubclem2  41860  rhmsubcALTVlem2  41879  xpprsng  41884  zlmodzxzscm  41909  gsumlsscl  41939  lincvalsng  41980  lincvalpr  41982  lincdifsn  41988  linc1  41989  lincellss  41990  difmodm1lt  42092  fdivmpt  42113  digexp  42180  amgmwlem  42299
  Copyright terms: Public domain W3C validator