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

Theorem impcom 411
Description: Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
Hypothesis
Ref Expression
imp.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
impcom ((𝜓𝜑) → 𝜒)

Proof of Theorem impcom
StepHypRef Expression
1 imp.1 . . 3 (𝜑 → (𝜓𝜒))
21com12 32 . 2 (𝜓 → (𝜑𝜒))
32imp 410 1 ((𝜓𝜑) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  mpan9  510  bianir  1054  19.29r  1875  19.41v  1950  19.41  2235  nfsb4t  2517  nfsb4tALT  2580  mo4  2625  2euexv  2693  2euex  2703  gencl  3481  2gencl  3482  vtocl2ga  3523  vtocl4g  3527  rspccva  3570  2reurex  3698  2reu1  3826  rexdifi  4073  sseq0  4307  r19.2z  4398  falseral0  4417  elelpwi  4509  preqsnd  4749  prproe  4798  ssuni  4825  disji2  5012  invdisjrab  5016  disjiun  5017  disjxiun  5027  trintss  5153  ssexg  5191  reusv2lem3  5266  propeqop  5362  otiunsndisj  5375  rexopabb  5380  pofun  5455  solin  5462  2optocl  5610  3optocl  5611  ssrelrn  5727  elrnmpt1  5794  resieq  5829  reuop  6112  funimaexg  6410  fnun  6434  fss  6501  fun  6514  fvelimab  6712  fvmptss  6757  fvn0ssdmfun  6819  fvcofneq  6836  fmptco  6868  funsndifnop  6890  fnressn  6897  fressnfv  6899  fvn0fvelrn  6902  fmptsng  6907  fvtp2g  6938  fvtp3g  6939  tpres  6940  fnex  6957  funfvima3  6976  isores3  7067  dmfex  7623  opreuopreu  7716  releldmdifi  7726  funeldmdif  7729  el2mpocsbcl  7763  f1o2ndf1  7801  frxp  7803  fnse  7810  ressuppssdif  7834  funsssuppss  7839  suppss  7843  mpoxopxnop0  7864  reldmtpos  7883  wfrfun  7948  wfrlem12  7949  smores  7972  tfrlem7  8002  tz7.48-2  8061  tz7.49  8064  oacl  8143  omcl  8144  oecl  8145  oarec  8171  oewordri  8201  oeworde  8202  oelim2  8204  oeoa  8206  oeoelem  8207  oeoe  8208  nnacl  8220  nnmcl  8221  nnecl  8222  nnmsucr  8234  2ecoptocl  8371  undifixp  8481  ssct  8581  xpf1o  8663  limensuc  8678  ac6sfi  8746  frfi  8747  difinf  8772  f1dmvrnfibi  8792  f1vrnfibi  8793  suppeqfsuppbi  8831  elfiun  8878  dffi3  8879  infsupprpr  8952  xpwdomg  9033  infdiffi  9105  epfrs  9157  rankxpsuc  9295  updjud  9347  tskwe  9363  infxpenlem  9424  fseqenlem1  9435  kmlem2  9562  nnadju  9608  cff1  9669  cflim2  9674  sornom  9688  infpssrlem4  9717  fin23lem26  9736  fin23lem30  9753  fin23lem34  9757  isf32lem11  9774  fin67  9806  isfin7-2  9807  fin1a2lem10  9820  axcc2lem  9847  axdc2lem  9859  axdc3lem2  9862  axdc3lem4  9864  axdc4lem  9866  iunfo  9950  tsk0  10174  gruina  10229  grur1a  10230  mulcanenq  10371  reclem2pr  10459  supsrlem  10522  supsr  10523  ax1rid  10572  negf1o  11059  mulgt1  11488  lbreu  11578  nnindd  11645  nnaddcl  11648  nnmulcl  11649  nn0n0n1ge2b  11951  nn0indd  12067  fzind  12068  fnn0ind  12069  uzaddcl  12292  uzinfi  12316  nn01to3  12329  elpq  12362  xmulasslem2  12663  supxrunb1  12700  supxrunb2  12701  infmremnf  12724  infmrp1  12725  uzsubsubfz  12924  elfz0ubfz0  13006  fz0fzdiffz0  13011  elfzmlbp  13013  fzofzim  13079  elfzom1elp1fzo  13099  ssfzo12bi  13127  fzonfzoufzol  13135  elfznelfzob  13138  injresinjlem  13152  injresinj  13153  modaddmodup  13297  modfzo0difsn  13306  modsumfzodifsn  13307  addmodlteq  13309  om2uzlti  13313  fsequb  13338  ssnn0fi  13348  ser1const  13422  expcllem  13436  expeq0  13455  expmordi  13527  expnngt1  13598  faclbnd  13646  hashf1rn  13709  hashgadd  13734  hashunx  13743  hashnn0n0nn  13748  hashgt0elex  13758  hashss  13766  hashfzp1  13788  hashxp  13791  hashmap  13792  hashimarni  13798  seqcoll  13818  hash2exprb  13825  hashge2el2difr  13835  elss2prb  13841  hashdifsnp1  13850  fi1uzind  13851  brfi1indALT  13854  lswlgt0cl  13912  swrdnd  14007  swrdnnn0nd  14009  swrdnd0  14010  swrd0  14011  swrdsbslen  14017  swrdspsleq  14018  pfxsuff1eqwrdeq  14052  swrdswrdlem  14057  swrdswrd  14058  wrd2ind  14076  pfxccatin12lem2a  14080  swrdccatin2  14082  pfxccatin12lem2  14084  pfxccatin12lem3  14085  pfxccatin12  14086  pfxccat3  14087  swrdccat  14088  pfxccat3a  14091  swrdccat3blem  14092  repswswrd  14137  repswrevw  14140  cshwmodn  14148  cshwsublen  14149  cshwidxmod  14156  cshwidxmodr  14157  cshf1  14163  2cshw  14166  cshweqrep  14174  cshw1  14175  2cshwcshw  14178  cshwcshid  14180  cshwcsh2id  14181  wrdlen2i  14295  2swrd2eqwrdeq  14306  wwlktovfo  14313  relexpsucnnl  14381  rtrclreclem3  14411  rtrclreclem4  14412  relexpindlem  14414  r19.29uz  14702  caubnd  14710  sqreu  14712  climshft  14925  climub  15010  climserle  15011  sumss  15073  sumss2  15075  modfsummods  15140  o1fsum  15160  binom  15177  climcndslem1  15196  climcndslem2  15197  pwm1geoserOLD  15217  cvgrat  15231  clim2prod  15236  prodfn0  15242  prodfrec  15243  ntrivcvgfvn0  15247  fprodn0  15325  fprodmodd  15343  fprodefsum  15440  demoivreALT  15546  ruclem8  15582  dvdsaddre2b  15649  dvdsdivcl  15658  dvdsfac  15668  oddnn02np1  15689  oddge22np1  15690  evennn02n  15691  evennn2n  15692  m1exp1  15717  nn0o  15724  pwp1fsum  15732  flodddiv4  15754  smu01lem  15824  dvdslegcd  15843  gcdneg  15860  dfgcd2  15884  gcdmultipleOLD  15890  seq1st  15905  alginv  15909  lcmf  15967  lcmftp  15970  lcmfunsnlem2lem2  15973  lcmfunsnlem  15975  lcmfun  15979  ncoprmgcdne1b  15984  coprmproddvdslem  15996  coprmproddvds  15997  cncongr1  16001  prmdvdsexp  16049  prmndvdsfaclt  16057  ncoprmlnprm  16058  fvprmselgcd1  16371  prmgaplem6  16382  prmgaplem7  16383  prmgaplem8  16384  cshwshashlem1  16421  setsstruct2  16513  setsstruct  16515  inveq  17036  catsubcat  17101  initoeu2lem0  17265  initoeu2lem1  17266  funcestrcsetclem8  17389  funcestrcsetclem9  17390  fthestrcsetc  17392  fullestrcsetc  17393  funcsetcestrclem9  17405  fthsetcestrc  17407  fullsetcestrc  17408  lubss  17723  lubel  17724  issstrmgm  17855  mgmb1mgm1  17857  sgrpidmnd  17908  frmdgsum  18019  smndex1mndlem  18066  mgm2nsgrplem3  18077  dfgrp2  18120  cyccom  18338  gaass  18419  gsumwrev  18486  symgextf1lem  18540  symgextf1  18541  fvcosymgeq  18549  gsmsymgreq  18552  symgfixelsi  18555  pmtrprfv3  18574  symggen  18590  pmtrprfval  18607  gsumzres  19022  gsumpr  19068  gsumzunsnd  19069  srgmulgass  19274  srgbinom  19288  lmodvsmmulgdi  19662  lmodfopnelem1  19663  rmodislmodlem  19694  0ringnnzr  20035  cnfldmulg  20123  cnfldexp  20124  psgndiflemB  20289  assamulgscm  20587  gsumply1subr  20863  gsummoncoe1  20933  pf1ind  20979  matmulcell  21050  mat1dimscm  21080  dmatmul  21102  dmatscmcl  21108  scmataddcl  21121  scmatsubcl  21122  scmatsgrp1  21127  mavmulsolcl  21156  ma1repveval  21176  1marepvmarrepid  21180  symgmatr01lem  21258  slesolvec  21284  cramerimplem2  21289  decpmatmullem  21376  pm2mpf1  21404  mp2pm2mplem4  21414  monmat2matmon  21429  chpscmat  21447  chpscmatgsumbin  21449  fvmptnn04ifb  21456  chfacfscmul0  21463  chfacfscmulgsum  21465  chfacfpmmul0  21467  chfacfpmmulgsum  21469  cpmadugsumlemF  21481  toprntopon  21530  clsss  21659  ntrss  21660  restntr  21787  cmpsublem  22004  cmpsub  22005  2ndcrest  22059  txindislem  22238  t0kq  22423  filufint  22525  fbflim2  22582  flftg  22601  alexsubALTlem4  22655  cnextfvval  22670  ustuqtop4  22850  xmettri2  22947  mettri  22959  metss  23115  tngngp3  23262  clmvscom  23695  lmmbr  23862  caublcls  23913  lmcau  23917  ovolunlem1a  24100  nulmbl2  24140  voliunlem1  24154  iunmbl  24157  volsup  24160  dvlip  24596  dvfsumle  24624  degltlem1  24673  ply1divex  24737  plyco  24838  dgrnznn  24844  dvnply2  24883  plydivex  24893  aannenlem2  24925  aaliou3lem2  24939  ulmcau  24990  zabsle1  25880  gausslemma2dlem1a  25949  gausslemma2dlem2  25951  gausslemma2dlem3  25952  gausslemma2dlem4  25953  2lgslem1a1  25973  2sqnn0  26022  2sqreulem1  26030  2sqreunnlem1  26033  dchrisumlem1  26073  dchrisumlem2  26074  dchrisumlem3  26075  qabvle  26209  ostthlem2  26212  ostth2lem2  26218  tgjustr  26268  axeuclidlem  26756  incistruhgr  26872  umgredgprv  26900  umgrpredgv  26933  usgredgprvALT  26985  uhgr2edg  26998  usgredg2vlem2  27016  lfuhgr1v0e  27044  subgrfun  27071  umgrres1lem  27100  upgrres1  27103  fusgrfis  27120  uhgrnbgr0nb  27144  nbgr1vtx  27148  nb3grprlem1  27170  uvtx01vtx  27187  fusgrn0degnn0  27289  vtxdginducedm1lem4  27332  finsumvtxdg2size  27340  wlkl1loop  27427  wlkres  27460  lfgrwlknloop  27479  pthdadjvtx  27519  upgr2pthnlp  27521  upgrwlkdvdelem  27525  upgrwlkdvde  27526  uhgrwkspthlem2  27543  usgr2trlspth  27550  usgr2pth  27553  pthdlem2lem  27556  lfgrn1cycl  27591  uspgrn2crct  27594  crctcshwlkn0lem3  27598  crctcshwlkn0lem4  27599  crctcshwlkn0lem5  27600  iswspthsnon  27642  wlkiswwlks1  27653  wlklnwwlkln1  27654  wlkiswwlks2  27661  wlkiswwlksupgr2  27663  wlklnwwlkln2lem  27668  wlknwwlksnbij  27674  wwlksnred  27678  wwlksnext  27679  wwlksnredwwlkn  27681  wwlksnredwwlkn0  27682  wwlksnextfun  27684  wwlksnextinj  27685  wwlksnextsurj  27686  wspthsnonn0vne  27703  wspn0  27710  wwlks2onv  27739  elwwlks2  27752  elwspths2spth  27753  rusgrnumwwlk  27761  clwwlkccatlem  27774  clwlkclwwlklem2a1  27777  clwlkclwwlklem2fv2  27781  clwlkclwwlklem2a4  27782  clwlkclwwlklem2a  27783  clwlkclwwlklem2  27785  clwlkclwwlkf1lem3  27791  clwwisshclwwslem  27799  clwwisshclwwsn  27801  erclwwlktr  27807  isclwwlknx  27821  clwwlkinwwlk  27825  clwwlkel  27831  clwwlkf  27832  clwwlkf1  27834  clwwlkfo  27835  clwwlkext2edg  27841  wwlksext2clwwlk  27842  wwlksubclwwlk  27843  clwwlknscsh  27847  erclwwlkntr  27856  eleclclwwlkn  27861  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  clwwlknon0  27878  clwwlknonel  27880  clwwlknon1  27882  clwwlknonwwlknonb  27891  clwwlknonex2lem2  27893  clwwlknun  27897  clwwlkvbij  27898  upgr3v3e3cycl  27965  uhgr3cyclex  27967  upgr4cycl4dv4e  27970  eulerpath  28026  eucrctshift  28028  eucrct2eupth  28030  1to2vfriswmgr  28064  1to3vfriswmgr  28065  3cyclfrgrrn1  28070  4cycl2vnunb  28075  frgrwopreglem2  28098  frgrwopreglem3  28099  frgrwopreglem5ALT  28107  fusgr2wsp2nb  28119  2clwwlk2clwwlklem  28131  2clwwlk2clwwlk  28135  numclwwlk1lem2f1  28142  numclwwlk1lem2fo  28143  numclwwlk1  28146  clwwlknonclwlknonf1o  28147  dlwwlknondlwlknonf1o  28150  numclwlk1  28156  numclwlk2lem2f  28162  numclwlk2lem2f1o  28164  numclwwlk5  28173  frgrreg  28179  frgrregord013  28180  friendship  28184  nsnlplig  28264  nsnlpligALT  28265  isgrpo  28280  vcdi  28348  vcdir  28349  vcass  28350  nmosetre  28547  hlim2  28975  shscli  29100  chintcli  29114  dfch2  29190  spansncvi  29435  nmopsetretALT  29646  nmfnsetre  29660  lnopl  29697  lnfnl  29714  pjss2coi  29947  pjorthcoi  29952  pjscji  29953  pjssdif2i  29957  pjclem4a  29981  pj3lem1  29989  strlem5  30038  hstrlem5  30046  cvmdi  30107  mdslmd3i  30115  atcv1  30163  atcvat4i  30180  cdj3lem2a  30219  cdj3lem3a  30222  opreu2reuALT  30247  iuninc  30324  disji2f  30340  disjif2  30344  fmptcof2  30420  xrsmulgzz  30712  ofldchr  30938  esumfzf  31438  issgon  31492  voliune  31598  volfiniune  31599  rrvsum  31822  bnj228  32115  bnj1294  32199  bnj229  32266  bnj607  32298  bnj908  32313  bnj953  32321  bnj1118  32366  bnj1174  32385  bnj1388  32415  funen1cnv  32467  acycgrsubgr  32518  cvmliftlem15  32658  satfsschain  32724  satfdm  32729  satf0op  32737  fmla0xp  32743  gonarlem  32754  goalrlem  32756  satffunlem1lem1  32762  satffunlem2lem1  32764  dmopab3rexdif  32765  satefvfmla0  32778  prv1n  32791  iprodefisumlem  33085  faclimlem1  33088  dfon2lem6  33146  tfisg  33168  poseq  33208  frrlem8  33243  fpr2  33253  frr2  33258  noprefixmo  33315  nosupbnd1lem5  33325  nocvxminlem  33360  nocvxmin  33361  slerec  33390  idinside  33658  onsucconni  33898  axc11n11r  34130  bj-brrelex12ALT  34483  bj-snmoore  34528  bj-finsumval0  34700  exlimim  34759  exellim  34761  icoreclin  34774  difunieq  34791  fvineqsneq  34829  pibt2  34834  wl-spae  34926  wl-aleq  34940  fin2so  35044  matunitlindf  35055  poimirlem4  35061  poimirlem26  35083  itg2addnclem  35108  upixp  35167  welb  35174  sdclem2  35180  metf1o  35193  sstotbnd3  35214  isbndx  35220  ismtycnv  35240  heiborlem4  35252  bfplem1  35260  opidonOLD  35290  grpomndo  35313  ax12eq  36237  ax12el  36238  cvrat4  36739  mzpexpmpt  39684  diophren  39752  rmxypos  39886  jm2.17a  39899  jm2.17b  39900  rmygeid  39903  jm2.18  39927  jm2.25  39938  jm2.15nn0  39942  jm2.16nn0  39943  pwslnm  40036  isnumbasgrplem1  40043  dgraalem  40087  relexpiidm  40403  relexpmulnn  40408  relexpmulg  40409  relexp01min  40412  relexp0a  40415  relexpxpmin  40416  clsk1indlem3  40744  grucollcld  40966  dvgrat  41014  radcnvrat  41016  sspwimpcf  41624  sspwimpcfVD  41625  e2ebindALT  41633  eu2ndop1stv  43679  afvfv0bi  43706  afveu  43707  afvres  43726  aovmpt4g  43755  ndmaovass  43760  ndmaovdistr  43761  afv2orxorb  43782  afv2eu  43792  imarnf1pr  43836  nltle2tri  43868  fzopredsuc  43878  subsubelfzo0  43881  fzoopth  43882  2ffzoeq  43883  smonoord  43886  elsetpreimafvssdm  43901  iccpartres  43933  iccpartiltu  43937  iccpartigtl  43938  iccpartgt  43942  icceuelpartlem  43950  fargshiftf1  43956  ichnreuop  43987  ichreuopeq  43988  elsprel  43990  sprsymrelfo  44012  prproropf1olem4  44021  paireqne  44026  sbcpr  44036  reupr  44037  goldbachth  44062  fmtnoprmfac1  44080  fmtnoprmfac2  44082  prmdvdsfmtnof1lem2  44100  lighneallem2  44122  lighneallem4  44126  requad2  44139  even3prm2  44235  fpprwpprb  44256  gbegt5  44277  sbgoldbwt  44293  sbgoldbm  44300  nnsum3primesgbe  44308  wtgoldbnnsum4prm  44318  bgoldbnnsum3prm  44320  bgoldbtbndlem2  44322  bgoldbtbndlem3  44323  bgoldbtbndlem4  44324  bgoldbtbnd  44325  isomuspgrlem1  44343  isomuspgrlem2d  44347  upgrwlkupwlk  44366  uspgropssxp  44370  uspgrsprfo  44374  mgmpropd  44393  isassintop  44468  lidldomn1  44543  lidlmmgm  44547  2zlidl  44556  2zrngamgm  44561  2zrngmmgm  44568  rnghmsscmap  44596  rnghmsubcsetclem2  44598  rngcinv  44603  rngccatidALTV  44611  rngcinvALTV  44615  funcrngcsetc  44620  funcrngcsetcALT  44621  rhmsscmap  44642  rhmsubcsetclem2  44644  rhmsubcrngclem2  44650  ringcinv  44654  funcringcsetc  44657  funcringcsetcALTV2lem9  44666  ringccatidALTV  44674  ringcinvALTV  44678  srhmsubc  44698  rhmsubclem4  44711  srhmsubcALTV  44716  rhmsubcALTVlem4  44729  lmodvsmdi  44782  ply1mulgsumlem1  44792  ply1mulgsumlem2  44793  lincdifsn  44831  lincsumcl  44838  lincscmcl  44839  lincext3  44863  lindslinindsimp1  44864  lindslinindsimp2lem5  44869  snlindsntor  44878  lincresunit2  44885  lincresunit3lem2  44887  zgtp1leeq  44928  m1modmmod  44933  elbigo2  44964  fllog2  44980  digexp  45019  dig1  45020  nn0sumshdiglemA  45031  nn0sumshdiglemB  45032  1arymaptf1  45054  2arymaptf1  45065  rrxlinec  45148  eenglngeehlnm  45151  rrx2linest  45154  itsclc0yqsol  45176  itsclc0xyqsol  45180
  Copyright terms: Public domain W3C validator