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

Theorem 3adant1 1099
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 1080 . 2 ((𝜃𝜑𝜓) → (𝜑𝜓))
2 3adant.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl 17 1 ((𝜃𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  3ad2ant2  1103  3ad2ant3  1104  eupickb  2567  sbciegft  3499  reuhyp  4926  funopg  5960  funprg  5978  funtpg  5980  funcnvtp  5989  fvun1  6308  fnreseql  6367  ftpg  6463  f13dfv  6570  mpt2eq3ia  6762  ordunel  7069  fex2  7163  poxp  7334  suppval1  7346  wfr3g  7458  smores3  7495  oaord  7672  oacan  7673  oaword  7674  omord  7693  omcan  7694  omwordri  7697  odi  7704  omass  7705  oeord  7713  oecan  7714  oewordri  7717  oeordsuc  7719  nnaord  7744  nnaordr  7745  nndi  7748  nnmass  7749  nnaword  7752  nnmord  7757  nnmwordri  7761  erov  7887  ecopovtrn  7893  ixpf  7972  mapxpen  8167  fimax2g  8247  unbnn  8257  funisfsupp  8321  inelfi  8365  elfiun  8377  sup0  8413  suppr  8418  infpr  8450  r111  8676  dif1card  8871  xpcdaen  9043  mapcdaen  9044  ackbij1lem16  9095  cff1  9118  cfflb  9119  cfsmolem  9130  fin23lem34  9206  hsmexlem2  9287  axcc3  9298  domtriomlem  9302  axdc3lem4  9313  axdc4lem  9315  axcclem  9317  konigthlem  9428  gchdomtri  9489  tskpr  9630  tskop  9631  tskuni  9643  tskun  9646  gruop  9665  gruun  9666  grudomon  9677  adderpqlem  9814  mulerpqlem  9815  addassnq  9818  mulassnq  9819  distrnq  9821  ltsonq  9829  ltanq  9831  ltmnq  9832  genpass  9869  distrlem1pr  9885  distrlem4pr  9886  ltsopr  9892  adddir  10069  axlttrn  10148  ltletr  10167  letr  10169  mul32  10241  mul31  10242  add32  10292  subsub23  10324  addsubass  10329  subcan2  10344  subsub2  10347  nppcan2  10350  sub32  10353  nnncan  10354  nnncan2  10356  pnpcan2  10359  subdi  10501  subdir  10502  receu  10710  mulcan1g  10718  mulcan2g  10719  divmul3  10728  divrec  10739  divrec2  10740  divsubdir  10759  divdiv1  10774  redivcl  10782  div2neg  10786  ltmul2  10912  lemul1  10913  lemul2  10914  lemul2a  10916  lediv1  10926  gt0div  10927  ge0div  10928  mulsuble0b  10933  ltdivmul  10936  ledivmul  10937  ltdivmul2  10938  ledivmul2  10940  lemuldiv  10941  ltdiv23  10952  lediv23  10953  ledivp1i  10987  ltdivp1i  10988  uzind2  11508  nn0ind  11510  fnn0ind  11514  uz3m2nn  11769  xrltletr  12026  xrletr  12027  xrre2  12039  xrltmin  12051  xrlemin  12053  xleadd2a  12122  xleadd1  12123  xltadd2  12125  xmulasslem3  12154  xmulass  12155  xltmul2  12161  ixxdisj  12228  iooneg  12330  iccneg  12331  icoshft  12332  icoshftf1o  12333  icodisj  12335  snunioo  12336  fzen  12396  ssfzunsnext  12424  fzrev3  12444  2ffzeq  12499  fzoaddel2  12563  elfzodifsumelfzo  12573  ssfzoulel  12602  ssfzo12bi  12603  fzoshftral  12625  adddivflid  12659  flltdivnn0lt  12674  ltdifltdiv  12675  fldiv4p1lem1div2  12676  modcyc  12745  modcyc2  12746  modaddabs  12748  modsubmodmod  12769  modaddmodup  12773  modaddmulmod  12777  moddi  12778  modsubdir  12779  expdiv  12951  digit2  13037  nfile  13188  hashdifpr  13241  hashreshashfun  13264  fi1uzind  13317  ccatass  13406  lswccatn0lsw  13409  swrdval  13462  swrdnd  13478  swrd0  13480  swrdfv2  13492  2swrd1eqwrdeq  13500  swrdswrdlem  13505  swrdccatin12lem2a  13531  swrdccatin12lem2b  13532  repswccat  13578  cshwidxmod  13595  cshwidxmodr  13596  cshf1  13602  repswcshw  13604  2cshw  13605  2cshwcom  13608  2cshwcshw  13617  cshwcsh2id  13620  ccatco  13627  2swrd2eqwrdeq  13742  wwlktovf  13745  brcnvtrclfv  13788  shftval2  13859  mulre  13905  absdiv  14079  absdiflt  14101  absdifle  14102  abs3dif  14115  cau3  14139  ello12r  14292  elo12r  14303  modfsummods  14569  geoisum1c  14655  rpnnen2lem4  14990  rpnnen2lem7  14993  dvdsmulc  15056  dvdsmulcr  15058  dvdsmultr1  15066  dvdsmultr2  15068  dvdssub2  15070  oexpneg  15116  divalgb  15174  ndvdsadd  15181  sadass  15240  modgcd  15300  dvdsgcd  15308  dvdsgcdb  15309  gcdass  15311  mulgcd  15312  absmulgcd  15313  rpmulgcd  15322  nn0seqcvgd  15330  algcvga  15339  lcmdvdsb  15373  lcmass  15374  lcmfunsnlem1  15397  lcmfunsnlem2lem1  15398  lcmfunsnlem2lem2  15399  coprmdvds  15413  coprmdvdsOLD  15414  coprmdvds2  15415  rpmul  15420  cncongr1  15428  cncongr2  15429  prmgt1  15456  qnumdenbi  15499  modprm0  15557  coprimeprodsq  15560  pythagtriplem4  15571  pythagtriplem8  15575  pythagtriplem9  15576  pythagtriplem12  15578  pythagtriplem14  15580  pythagtriplem16  15582  pcpremul  15595  pcgcd  15629  vdwapval  15724  vdwapun  15725  prmgaplem3  15804  prmgaplem4  15805  prmgaplem7  15808  prmgapprmolem  15812  setsstructOLD  15946  mreiincl  16303  mreincl  16306  mremre  16311  mrcss  16323  catcisolem  16803  pleval2  17012  pospo  17020  latlem  17096  latjcom  17106  latmcom  17122  lubss  17168  lubun  17170  clatglbss  17174  ipole  17205  ipolt  17206  pslem  17253  dirtr  17283  gsumws2  17426  frmdmnd  17443  isgrpi  17492  grpsubrcan  17543  grpinvsub  17544  grpsubeq0  17548  grpsubadd0sub  17549  grpnpcan  17554  qussub  17701  ghmsub  17715  symggrp  17866  symgextsymg  17890  gsmsymgreqlem2  17897  symgfixfolem1  17904  pmtrprfv3  17920  symggen  17936  lsmass  18129  efgsrel  18193  cntzcmn  18291  dvrcl  18732  unitdvcl  18733  dvrcan1  18737  subrgmre  18852  abvsubtri  18883  abvtrivd  18888  lmodvsubval2  18966  rmodislmodlem  18978  rmodislmod  18979  lss0cl  18995  lssintcl  19012  lssincl  19013  reslmhm2  19101  lspvadd  19144  lspsntrim  19146  islbs3  19203  rrgeq0  19338  evlsval2  19568  cncrng  19815  xrsmcmn  19817  cndrng  19823  cnsrng  19828  xrs1mnd  19832  absabv  19851  psgnco  19977  zrhpsgninv  19979  zrhpsgnevpm  19985  zrhpsgnodpm  19986  zrhpsgnelbas  19988  zrhcopsgnelbas  19989  uvcresum  20180  lindfmm  20214  lindsmm  20215  mamudm  20242  mamufacex  20243  matsubgcell  20288  matsc  20304  scmatscmide  20361  scmatrhmcl  20382  1marepvsma1  20437  m1detdiag  20451  mdetralt  20462  m2detleiblem7  20481  gsummatr01lem3  20511  gsummatr01  20513  smadiadetlem0  20515  decpmate  20619  decpmatcl  20620  pm2mpcl  20650  pm2mpghmlem2  20665  chfacfscmul0  20711  chfacfscmulgsum  20713  chfacfpmmul0  20715  chfacfpmmulgsum  20717  unopn  20756  clsss  20906  cldmre  20930  toponmre  20945  opnssneib  20967  restabs  21017  restcls  21033  restntr  21034  hausnei2  21205  cmpsublem  21250  bwth  21261  hausmapdom  21351  ptpjcn  21462  upxp  21474  ptrescn  21490  xkopjcn  21507  fbssfi  21688  snfil  21715  ufprim  21760  rnelfm  21804  flimrest  21834  fclsrest  21875  tmdgsum  21946  blpnfctr  22288  mscl  22313  xmscl  22314  xmsge0  22315  xmseq0  22316  restmetu  22422  ngpds  22455  tngngp3  22507  unitnmn0  22519  xrsxmet  22659  metds0  22700  cncfmptc  22761  isclmp  22943  cnlmod  22986  ncvsi  22997  cphsqrtcl  23030  cfil3i  23113  cfilres  23140  cmmbl  23348  voliunlem2  23365  itg2ub  23545  itgrecl  23609  tdeglem3  23864  r1pid  23964  eflogeq  24393  cxpadd  24470  logbchbase  24554  relogbreexp  24558  relogbzexp  24559  relogbmulexp  24561  logbleb  24566  logblt  24567  lawcos  24591  pythag  24592  asinsinb  24669  acoscosb  24670  atantanb  24696  amgmlem  24761  lgsneg  25091  lgsne0  25105  lgsmodeq  25112  lgsmulsqcoprm  25113  gausslemma2dlem1a  25135  brbtwn2  25830  colinearalg  25835  eleesubd  25837  axcgrrflx  25839  axcgrtr  25840  axsegcon  25852  ax5seglem1  25853  ax5seglem2  25854  ax5seglem4  25857  axbtwnid  25864  axlowdimlem14  25880  axlowdim  25886  axcontlem5  25893  axcontlem7  25895  funvtxdmge2valOLD  25944  funiedgdmge2valOLD  25945  usgr1v0e  26263  nb3grprlem2  26327  cplgr3v  26387  cusgrsizeindslem  26403  sizusglecusglem2  26414  umgr2v2e  26477  cusgrrusgr  26533  iswlk  26562  edginwlk  26586  uspgr2wlkeq  26598  uspgr2wlkeq2  26599  uspgr2wlkeqi  26600  wlkon2n0  26618  pthdadjvtx  26682  upgr2pthnlp  26684  spthonepeq  26704  pthdlem2lem  26719  crctcshwlkn0lem3  26760  crctcshwlkn0lem5  26762  wlkiswwlks2lem4  26826  wlkiswwlks2lem6  26828  wlklnwwlkln2lem  26836  wwlksnred  26855  wwlksnextbi  26857  wwlksnextwrd  26860  2pthdlem1  26895  2wlkdlem10  26900  umgr2adedgwlkonALT  26912  elwwlks2s3  26916  elwwlks2ons3im  26919  elwwlks2ons3OLD  26921  s3wwlks2on  26922  2wspdisj  26929  2wspiundisj  26930  clwwlkgt0  26954  clwlkclwwlklem2a4  26963  clwlkclwwlklem2a  26964  clwlkclwwlk  26968  clwlkclwwlk2  26969  clwwisshclwwslemlem  26970  erclwwlktr  26979  clwwlkf  27010  wwlksubclwwlk  27023  erclwwlkntr  27035  clwlksfclwwlk  27049  clwwlknon  27063  clwwlknonwwlknonbOLD  27081  frcond1  27246  frgr3v  27255  3vfriswmgr  27258  frgrwopreglem4a  27290  frrusgrord0lem  27319  2clwwlk2clwwlklem1  27327  extwwlkfab  27342  numclwlk1lem2f1  27347  numclwlk1lem2fo  27348  numclwwlk2lem1  27356  numclwlk2lem2f  27357  numclwlk2lem2f1o  27359  numclwwlk2  27361  numclwwlk2lem1OLD  27363  numclwlk2lem2fOLD  27364  numclwlk2lem2f1oOLD  27366  numclwwlk2OLD  27368  frgrreggt1  27380  friendshipgt3  27385  imsmetlem  27673  nmoxr  27749  nmoolb  27754  blometi  27786  phpar2  27806  phpar  27807  ipasslem5  27818  hvadd32  28019  hvaddsub12  28023  hvaddsubass  28026  hvsubass  28029  hvsub32  28030  hvsubdistr1  28034  hvsubdistr2  28035  hvmulcan  28057  hvmulcan2  28058  hvsubcan  28059  his5  28071  his2sub  28077  hhssabloilem  28246  hhssnv  28249  shlej2  28348  pjoi0  28704  hodcl  28734  hoadd32  28770  hosubdi  28795  hosubsub2  28799  hoaddsubass  28802  hosubsub4  28805  nmoplb  28894  unop  28902  hmop  28909  nmfnlb  28911  lnopmul  28954  kbass1  29103  kbass2  29104  leopmul2i  29122  leoptr  29124  cvntr  29279  mdslmd4i  29320  mdexchi  29322  atcv1  29367  sumdmdii  29402  fcoinvbr  29545  fpwrelmapffs  29637  xreceu  29758  isinftm  29863  unitdivcld  30075  esummulc1  30271  hasheuni  30275  unelsiga  30325  inelpisys  30345  carsgsigalem  30505  signswmnd  30762  bnj545  31091  bnj594  31108  bnj1311  31218  cvmsf1o  31380  cvmscld  31381  lediv2aALT  31697  subdivcomb2  31738  gcd32  31763  fununiq  31793  trpredpo  31859  poseq  31878  frr3g  31904  sltres  31940  sltletr  32006  sletr  32008  nocvxmin  32019  dfrdg4  32183  brcolinear  32291  colinearex  32292  nn0prpwlem  32442  clsun  32448  fnemeet1  32486  fnemeet2  32487  fnejoin1  32488  fnejoin2  32489  eltail  32494  rdgeqoa  33348  curf  33517  poimirlem28  33567  cnambfre  33588  ftc1anclem4  33618  cocanfo  33642  f1ocan1fv  33651  metf1o  33681  ismtybnd  33736  ghomco  33820  isdrngo2  33887  inidl  33959  igenmin  33993  brxrn  34276  cmtvalN  34816  cvrval  34874  pmapmeet  35377  paddval  35402  paddssat  35418  elpcliN  35497  pclssN  35498  pclunN  35502  paddunN  35531  poldmj1N  35532  tendoplcl2  36383  tendoplcl  36386  dihmeet  36949  mapco2g  37594  mzpcompact2lem  37631  eqrabdioph  37658  lerabdioph  37686  eluzrabdioph  37687  ltrabdioph  37689  nerabdioph  37690  dvdsrabdioph  37691  reglogcl  37771  rmxyadd  37803  rmyabs  37842  congadd  37850  congabseq  37858  rmydioph  37898  mendring  38079  mendlmod  38080  iocinico  38114  relexp0a  38325  relexpaddss  38327  brcoffn  38645  dvconstbi  38850  uzwo4  39535  ssin0  39537  ssinc  39578  ssdec  39579  unima  39660  fvmpt2bd  39664  disjf1o  39692  ssnnf1octb  39696  sub31  39817  fperiodmullem  39831  ssfiunibd  39837  infxr  39896  fmul01  40130  islptre  40169  lptre2pt  40190  limcleqr  40194  limclner  40201  limsuppnflem  40260  limsupvaluz2  40288  supcnvlimsup  40290  xlimmnfvlem2  40377  xlimmnfv  40378  xlimpnfvlem2  40381  xlimpnfv  40382  climxlim2lem  40389  coskpi2  40395  cosknegpi  40398  dvnmptdivc  40471  dvdsn1add  40472  dvnmptconst  40474  dvmptfprod  40478  dvnprodlem1  40479  dvnprodlem2  40480  ovolsplit  40523  stoweidlem60  40595  stowei  40599  dirkeritg  40637  fourierdlem70  40711  fourierdlem71  40712  fourierdlem103  40744  fourierdlem104  40745  fouriersw  40766  rrxtopnfi  40824  saluncl  40855  salexct  40870  sge0ltfirp  40935  sge0iunmpt  40953  meadjiunlem  41000  meaiuninc3v  41019  carageniuncllem1  41056  caratheodorylem1  41061  ovncvrrp  41099  ovnsubaddlem1  41105  hspmbllem2  41162  ovolval5lem3  41189  smfpimbor1lem1  41326  smfsuplem1  41338  smflimsuplem4  41350  sigarls  41367  cnambpcma  41634  elfzelfzlble  41656  fzoopth  41662  m1mod0mod1  41664  fsumsplitsndif  41668  iccpartiltu  41683  pfxsuff1eqwrdeq  41732  ccatpfx  41734  pfx2  41737  pfxccatin12lem1  41748  fmtno4prmfac  41809  2pwp1prmfmtno  41829  lighneallem4b  41851  oexpnegALTV  41913  mogoldbblem  41954  gbegt5  41974  sbgoldbm  41997  nnsum3primesle9  42007  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  evengpoap3  42012  nnsum4primesevenALTV  42014  isupwlk  42042  lidldomnnring  42255  2zrngacmnd  42267  rhmsubclem2  42412  rhmsubcALTVlem2  42430  xpprsng  42435  zlmodzxzscm  42460  gsumlsscl  42489  lincvalsng  42530  lincvalpr  42532  lincdifsn  42538  linc1  42539  lincellss  42540  difmodm1lt  42642  fdivmpt  42659  digexp  42726  amgmwlem  42876
  Copyright terms: Public domain W3C validator