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

Theorem 3adant1 1078
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 1059 . 2 ((𝜃𝜑𝜓) → (𝜑𝜓))
2 3adant.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl 17 1 ((𝜃𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1037
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 197  df-an 386  df-3an 1039
This theorem is referenced by:  3ad2ant2  1082  3ad2ant3  1083  eupickb  2537  sbciegft  3464  reuhyp  4894  funopg  5920  funprg  5938  funtpg  5940  funcnvtp  5949  fvun1  6267  fnreseql  6325  ftpg  6420  f13dfv  6527  mpt2eq3ia  6717  ordunel  7024  fex2  7118  poxp  7286  suppval1  7298  wfr3g  7410  smores3  7447  oaord  7624  oacan  7625  oaword  7626  omord  7645  omcan  7646  omwordri  7649  odi  7656  omass  7657  oeord  7665  oecan  7666  oewordri  7669  oeordsuc  7671  nnaord  7696  nnaordr  7697  nndi  7700  nnmass  7701  nnaword  7704  nnmord  7709  nnmwordri  7713  erov  7841  ecopovtrn  7847  ixpf  7927  mapxpen  8123  fimax2g  8203  unbnn  8213  funisfsupp  8277  inelfi  8321  elfiun  8333  sup0  8369  suppr  8374  infpr  8406  r111  8635  dif1card  8830  xpcdaen  9002  mapcdaen  9003  ackbij1lem16  9054  cff1  9077  cfflb  9078  cfsmolem  9089  fin23lem34  9165  hsmexlem2  9246  axcc3  9257  domtriomlem  9261  axdc3lem4  9272  axdc4lem  9274  axcclem  9276  konigthlem  9387  gchdomtri  9448  tskpr  9589  tskop  9590  tskuni  9602  tskun  9605  gruop  9624  gruun  9625  grudomon  9636  adderpqlem  9773  mulerpqlem  9774  addassnq  9777  mulassnq  9778  distrnq  9780  ltsonq  9788  ltanq  9790  ltmnq  9791  genpass  9828  distrlem1pr  9844  distrlem4pr  9845  ltsopr  9851  adddir  10028  axlttrn  10107  ltletr  10126  letr  10128  mul32  10200  mul31  10201  add32  10251  subsub23  10283  addsubass  10288  subcan2  10303  subsub2  10306  nppcan2  10309  sub32  10312  nnncan  10313  nnncan2  10315  pnpcan2  10318  subdi  10460  subdir  10461  receu  10669  mulcan1g  10677  mulcan2g  10678  divmul3  10687  divrec  10698  divrec2  10699  divsubdir  10718  divdiv1  10733  redivcl  10741  div2neg  10745  ltmul2  10871  lemul1  10872  lemul2  10873  lemul2a  10875  lediv1  10885  gt0div  10886  ge0div  10887  mulsuble0b  10892  ltdivmul  10895  ledivmul  10896  ltdivmul2  10897  ledivmul2  10899  lemuldiv  10900  ltdiv23  10911  lediv23  10912  ledivp1i  10946  ltdivp1i  10947  uzind2  11467  nn0ind  11469  fnn0ind  11473  uz3m2nn  11728  xrltletr  11985  xrletr  11986  xrre2  11998  xrltmin  12010  xrlemin  12012  xleadd2a  12081  xleadd1  12082  xltadd2  12084  xmulasslem3  12113  xmulass  12114  xltmul2  12120  ixxdisj  12187  iooneg  12289  iccneg  12290  icoshft  12291  icoshftf1o  12292  icodisj  12294  snunioo  12295  fzen  12355  ssfzunsnext  12383  fzrev3  12403  2ffzeq  12456  fzoaddel2  12519  elfzodifsumelfzo  12529  ssfzoulel  12558  ssfzo12bi  12559  fzoshftral  12580  adddivflid  12614  flltdivnn0lt  12629  ltdifltdiv  12630  fldiv4p1lem1div2  12631  modcyc  12700  modcyc2  12701  modaddabs  12703  modsubmodmod  12724  modaddmodup  12728  modaddmulmod  12732  moddi  12733  modsubdir  12734  expdiv  12906  digit2  12992  nfile  13145  hashdifpr  13198  hashreshashfun  13221  fi1uzind  13274  fi1uzindOLD  13280  ccatass  13366  lswccatn0lsw  13368  swrdval  13411  swrdnd  13426  swrd0  13428  swrdfv2  13440  2swrd1eqwrdeq  13448  swrdswrdlem  13453  swrdccatin12lem2a  13479  swrdccatin12lem2b  13480  repswccat  13526  cshwidxmod  13543  cshwidxmodr  13544  cshf1  13550  repswcshw  13552  2cshw  13553  2cshwcom  13556  2cshwcshw  13565  cshwcsh2id  13568  ccatco  13575  2swrd2eqwrdeq  13690  wwlktovf  13693  brcnvtrclfv  13738  shftval2  13809  mulre  13855  absdiv  14029  absdiflt  14051  absdifle  14052  abs3dif  14065  cau3  14089  ello12r  14242  elo12r  14253  modfsummods  14519  geoisum1c  14605  rpnnen2lem4  14940  rpnnen2lem7  14943  dvdsmulc  15003  dvdsmulcr  15005  dvdsmultr1  15013  dvdsmultr2  15015  dvdssub2  15017  oexpneg  15063  divalgb  15121  ndvdsadd  15128  sadass  15187  modgcd  15247  dvdsgcd  15255  dvdsgcdb  15256  gcdass  15258  mulgcd  15259  absmulgcd  15260  rpmulgcd  15269  nn0seqcvgd  15277  algcvga  15286  lcmdvdsb  15320  lcmass  15321  lcmfunsnlem1  15344  lcmfunsnlem2lem1  15345  lcmfunsnlem2lem2  15346  coprmdvds  15360  coprmdvdsOLD  15361  coprmdvds2  15362  rpmul  15367  cncongr1  15375  cncongr2  15376  prmgt1  15403  qnumdenbi  15446  modprm0  15504  coprimeprodsq  15507  pythagtriplem4  15518  pythagtriplem8  15522  pythagtriplem9  15523  pythagtriplem12  15525  pythagtriplem14  15527  pythagtriplem16  15529  pcpremul  15542  pcgcd  15576  vdwapval  15671  vdwapun  15672  prmgaplem3  15751  prmgaplem4  15752  prmgaplem7  15755  prmgapprmolem  15759  setsstructOLD  15893  mreiincl  16250  mreincl  16253  mremre  16258  mrcss  16270  catcisolem  16750  pleval2  16959  pospo  16967  latlem  17043  latjcom  17053  latmcom  17069  lubss  17115  lubun  17117  clatglbss  17121  ipole  17152  ipolt  17153  pslem  17200  dirtr  17230  gsumws2  17373  frmdmnd  17390  isgrpi  17439  grpsubrcan  17490  grpinvsub  17491  grpsubeq0  17495  grpsubadd0sub  17496  grpnpcan  17501  qussub  17648  ghmsub  17662  symggrp  17814  symgextsymg  17838  gsmsymgreqlem2  17845  symgfixfolem1  17852  pmtrprfv3  17868  symggen  17884  lsmass  18077  efgsrel  18141  cntzcmn  18239  dvrcl  18680  unitdvcl  18681  dvrcan1  18685  subrgmre  18798  abvsubtri  18829  abvtrivd  18834  lmodvsubval2  18912  rmodislmodlem  18924  rmodislmod  18925  lss0cl  18941  lssintcl  18958  lssincl  18959  reslmhm2  19047  lspvadd  19090  lspsntrim  19092  islbs3  19149  rrgeq0  19284  evlsval2  19514  cncrng  19761  xrsmcmn  19763  cndrng  19769  cnsrng  19774  xrs1mnd  19778  absabv  19797  psgnco  19923  zrhpsgninv  19925  zrhpsgnevpm  19931  zrhpsgnodpm  19932  zrhpsgnelbas  19934  zrhcopsgnelbas  19935  uvcresum  20126  lindfmm  20160  lindsmm  20161  mamudm  20188  mamufacex  20189  matsubgcell  20234  matsc  20250  scmatscmide  20307  scmatrhmcl  20328  1marepvsma1  20383  m1detdiag  20397  mdetralt  20408  m2detleiblem7  20427  gsummatr01lem3  20457  gsummatr01  20459  smadiadetlem0  20461  decpmate  20565  decpmatcl  20566  pm2mpcl  20596  pm2mpghmlem2  20611  chfacfscmul0  20657  chfacfscmulgsum  20659  chfacfpmmul0  20661  chfacfpmmulgsum  20663  unopn  20702  clsss  20852  cldmre  20876  toponmre  20891  opnssneib  20913  restabs  20963  restcls  20979  restntr  20980  hausnei2  21151  cmpsublem  21196  bwth  21207  hausmapdom  21297  ptpjcn  21408  upxp  21420  ptrescn  21436  xkopjcn  21453  fbssfi  21635  snfil  21662  ufprim  21707  rnelfm  21751  flimrest  21781  fclsrest  21822  tmdgsum  21893  blpnfctr  22235  mscl  22260  xmscl  22261  xmsge0  22262  xmseq0  22263  restmetu  22369  ngpds  22402  tngngp3  22454  unitnmn0  22466  xrsxmet  22606  metds0  22647  cncfmptc  22708  isclmp  22891  cnlmod  22934  ncvsi  22945  cphsqrtcl  22978  cfil3i  23061  cfilres  23088  cmmbl  23296  voliunlem2  23313  itg2ub  23494  itgrecl  23558  tdeglem3  23813  r1pid  23913  eflogeq  24342  cxpadd  24419  logbchbase  24503  relogbreexp  24507  relogbzexp  24508  relogbmulexp  24510  logbleb  24515  logblt  24516  lawcos  24540  pythag  24541  asinsinb  24618  acoscosb  24619  atantanb  24645  amgmlem  24710  lgsneg  25040  lgsne0  25054  lgsmodeq  25061  lgsmulsqcoprm  25062  gausslemma2dlem1a  25084  brbtwn2  25779  colinearalg  25784  eleesubd  25786  axcgrrflx  25788  axcgrtr  25789  axsegcon  25801  ax5seglem1  25802  ax5seglem2  25803  ax5seglem4  25806  axbtwnid  25813  axlowdimlem14  25829  axlowdim  25835  axcontlem5  25842  axcontlem7  25844  funvtxdmge2valOLD  25893  funiedgdmge2valOLD  25894  usgr1v0e  26212  nb3grprlem2  26277  cplgr3v  26325  cusgrsizeindslem  26341  sizusglecusglem2  26352  umgr2v2e  26415  cusgrrusgr  26471  iswlk  26500  edginwlk  26524  uspgr2wlkeq  26536  uspgr2wlkeq2  26537  uspgr2wlkeqi  26538  wlkon2n0  26556  pthdadjvtx  26620  upgr2pthnlp  26622  spthonepeq  26642  pthdlem2lem  26657  crctcshwlkn0lem3  26698  crctcshwlkn0lem5  26700  wlkiswwlks2lem4  26752  wlkiswwlks2lem6  26754  wlklnwwlkln2lem  26762  wwlksnred  26781  wwlksnextbi  26783  wwlksnextwrd  26786  2pthdlem1  26820  2wlkdlem10  26825  umgr2adedgwlkonALT  26837  elwwlks2ons3  26842  s3wwlks2on  26843  elwspths2on  26847  2wspdisj  26849  2wspiundisj  26850  clwwlknp  26881  isclwwlksng  26882  clwlkclwwlklem2a4  26892  clwlkclwwlklem2a  26893  clwlkclwwlk  26897  clwlkclwwlk2  26898  clwwlksgt0  26899  clwwlksf  26908  wwlksubclwwlks  26918  clwwisshclwwslemlem  26919  erclwwlkstr  26929  erclwwlksntr  26941  clwlksfclwwlk  26955  frcond1  27123  frgr3v  27132  3vfriswmgr  27135  frrusgrord0lem  27190  extwwlkfablem2lem  27194  numclwwlkffin  27199  numclwwlkovfel2  27201  numclwwlkovf2ex  27204  extwwlkfab  27207  numclwlk1lem2f1  27211  numclwlk1lem2fo  27212  numclwwlk2lem1  27219  numclwlk2lem2f  27220  numclwlk2lem2f1o  27222  numclwwlk2  27224  frgrreggt1  27235  friendshipgt3  27240  imsmetlem  27529  nmoxr  27605  nmoolb  27610  blometi  27642  phpar2  27662  phpar  27663  ipasslem5  27674  hvadd32  27875  hvaddsub12  27879  hvaddsubass  27882  hvsubass  27885  hvsub32  27886  hvsubdistr1  27890  hvsubdistr2  27891  hvmulcan  27913  hvmulcan2  27914  hvsubcan  27915  his5  27927  his2sub  27933  hhssabloilem  28102  hhssnv  28105  shlej2  28204  pjoi0  28560  hodcl  28590  hoadd32  28626  hosubdi  28651  hosubsub2  28655  hoaddsubass  28658  hosubsub4  28661  nmoplb  28750  unop  28758  hmop  28765  nmfnlb  28767  lnopmul  28810  kbass1  28959  kbass2  28960  leopmul2i  28978  leoptr  28980  cvntr  29135  mdslmd4i  29176  mdexchi  29178  atcv1  29223  sumdmdii  29258  fcoinvbr  29403  fpwrelmapffs  29494  xreceu  29615  isinftm  29720  unitdivcld  29932  esummulc1  30128  hasheuni  30132  unelsiga  30182  inelpisys  30202  carsgsigalem  30362  signswmnd  30619  bnj545  30950  bnj594  30967  bnj1311  31077  cvmsf1o  31239  cvmscld  31240  lediv2aALT  31556  subdivcomb2  31598  gcd32  31623  fununiq  31653  trpredpo  31719  poseq  31734  frr3g  31763  sltres  31799  sltletr  31865  sletr  31867  nocvxmin  31878  dfrdg4  32042  brcolinear  32150  colinearex  32151  nn0prpwlem  32301  clsun  32307  fnemeet1  32345  fnemeet2  32346  fnejoin1  32347  fnejoin2  32348  eltail  32353  rdgeqoa  33198  curf  33367  poimirlem28  33417  cnambfre  33438  ftc1anclem4  33468  cocanfo  33492  f1ocan1fv  33501  metf1o  33531  ismtybnd  33586  ghomco  33670  isdrngo2  33737  inidl  33809  igenmin  33843  cmtvalN  34324  cvrval  34382  pmapmeet  34885  paddval  34910  paddssat  34926  elpcliN  35005  pclssN  35006  pclunN  35010  paddunN  35039  poldmj1N  35040  tendoplcl2  35892  tendoplcl  35895  dihmeet  36458  mapco2g  37103  mzpcompact2lem  37140  eqrabdioph  37167  lerabdioph  37195  eluzrabdioph  37196  ltrabdioph  37198  nerabdioph  37199  dvdsrabdioph  37200  reglogcl  37280  rmxyadd  37312  rmyabs  37351  congadd  37359  congabseq  37367  rmydioph  37407  mendring  37588  mendlmod  37589  iocinico  37623  relexp0a  37834  relexpaddss  37836  brcoffn  38154  dvconstbi  38359  uzwo4  39047  ssin0  39049  ssinc  39090  ssdec  39091  unima  39168  fvmpt2bd  39172  disjf1o  39200  ssnnf1octb  39204  sub31  39322  fperiodmullem  39336  ssfiunibd  39342  infxr  39402  fmul01  39618  islptre  39657  lptre2pt  39678  limcleqr  39682  limclner  39689  limsuppnflem  39748  limsupvaluz2  39776  supcnvlimsup  39778  coskpi2  39846  cosknegpi  39849  dvnmptdivc  39922  dvdsn1add  39923  dvnmptconst  39925  dvmptfprod  39929  dvnprodlem1  39930  dvnprodlem2  39931  ovolsplit  39974  stoweidlem60  40046  stowei  40050  dirkeritg  40088  fourierdlem70  40162  fourierdlem71  40163  fourierdlem103  40195  fourierdlem104  40196  fouriersw  40217  rrxtopnfi  40275  saluncl  40306  salexct  40321  sge0ltfirp  40386  sge0iunmpt  40404  meadjiunlem  40451  carageniuncllem1  40504  caratheodorylem1  40509  ovncvrrp  40547  ovnsubaddlem1  40553  hspmbllem2  40610  ovolval5lem3  40637  smfpimbor1lem1  40774  smfsuplem1  40786  smflimsuplem4  40798  sigarls  40815  cnambpcma  41078  elfzelfzlble  41100  fzoopth  41106  m1mod0mod1  41109  fsumsplitsndif  41113  iccpartiltu  41128  pfxsuff1eqwrdeq  41178  ccatpfx  41180  pfx2  41183  pfxccatin12lem1  41194  fmtno4prmfac  41255  2pwp1prmfmtno  41275  lighneallem4b  41297  oexpnegALTV  41359  mogoldbblem  41400  gbegt5  41420  sbgoldbm  41443  nnsum3primesle9  41453  nnsum4primesodd  41455  nnsum4primesoddALTV  41456  evengpoap3  41458  nnsum4primesevenALTV  41460  isupwlk  41488  lidldomnnring  41701  2zrngacmnd  41713  rhmsubclem2  41858  rhmsubcALTVlem2  41876  xpprsng  41881  zlmodzxzscm  41906  gsumlsscl  41935  lincvalsng  41976  lincvalpr  41978  lincdifsn  41984  linc1  41985  lincellss  41986  difmodm1lt  42088  fdivmpt  42105  digexp  42172  amgmwlem  42319
  Copyright terms: Public domain W3C validator