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

Theorem impcom 445
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 444 1 ((𝜓𝜑) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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
This theorem is referenced by:  mpan9  487  bianir  1047  19.29r  1951  19.41v  2026  19.41vOLD  2079  19.41  2250  nfsb4t  2526  2euex  2682  gencl  3375  2gencl  3376  vtocl4g  3417  rspccva  3448  sseq0  4118  minelOLD  4178  r19.2z  4204  falseral0  4225  elelpwi  4315  eqoreldifOLD  4370  preqsnd  4536  prproe  4586  ssuni  4611  ssuniOLD  4612  disji2  4788  invdisjrab  4791  disjiun  4792  disjxiun  4801  trintss  4921  ssexg  4956  reusv2lem3  5020  propeqop  5118  otiunsndisj  5130  pofun  5203  solin  5210  2optocl  5353  3optocl  5354  ssrelrn  5470  elrnmpt1  5529  resieq  5565  funimaexg  6136  fnun  6158  fss  6217  fun  6227  fvelimab  6416  fvmptss  6455  fvn0ssdmfun  6514  fvcofneq  6531  fmptco  6560  funsndifnop  6580  fnressn  6589  fressnfv  6591  fvn0fvelrn  6594  fmptsng  6599  fvtp2g  6629  fvtp3g  6630  tpres  6631  fnex  6646  funfvima3  6659  isores3  6749  dmfex  7290  el2mpt2csbcl  7419  f1o2ndf1  7454  frxp  7456  fnse  7463  ressuppssdif  7485  funsssuppss  7491  suppss  7495  mpt2xopxnop0  7511  reldmtpos  7530  wfrfun  7595  wfrlem12  7596  smores  7619  tfrlem7  7649  tz7.48-2  7707  tz7.49  7710  oacl  7786  omcl  7787  oecl  7788  oarec  7813  oewordri  7843  oeworde  7844  oelim2  7846  oeoa  7848  oeoelem  7849  oeoe  7850  nnacl  7862  nnmcl  7863  nnecl  7864  nnmsucr  7876  2ecoptocl  8007  undifixp  8112  ssct  8208  xpf1o  8289  limensuc  8304  ac6sfi  8371  frfi  8372  difinf  8397  f1dmvrnfibi  8417  f1vrnfibi  8418  suppeqfsuppbi  8456  elfiun  8503  dffi3  8504  xpwdomg  8657  preleqOLD  8689  infdiffi  8730  epfrs  8782  rankxpsuc  8920  updjud  8970  tskwe  8986  infxpenlem  9046  fseqenlem1  9057  kmlem2  9185  cff1  9292  cflim2  9297  sornom  9311  infpssrlem4  9340  fin23lem26  9359  fin23lem30  9376  fin23lem34  9380  isf32lem11  9397  fin67  9429  isfin7-2  9430  fin1a2lem10  9443  axcc2lem  9470  axdc2lem  9482  axdc3lem2  9485  axdc3lem4  9487  axdc4lem  9489  iunfo  9573  tsk0  9797  gruina  9852  grur1a  9853  mulcanenq  9994  reclem2pr  10082  supsrlem  10144  supsr  10145  ax1rid  10194  negf1o  10672  mulgt1  11094  fiminre  11184  lbreu  11185  nnaddcl  11254  nnmulcl  11255  nn0n0n1ge2b  11571  nn0indd  11686  fzind  11687  fnn0ind  11688  uzaddcl  11957  uzinfi  11981  nn01to3  11994  xmulasslem2  12325  supxrunb1  12362  supxrunb2  12363  infmremnf  12386  infmrp1  12387  uzsubsubfz  12576  elfz0ubfz0  12657  fz0fzdiffz0  12662  elfzmlbp  12664  fzofzim  12729  elfzom1elp1fzo  12749  elfzom1p1elfzo  12762  ssfzo12bi  12777  fzonfzoufzol  12785  elfznelfzob  12788  injresinjlem  12802  injresinj  12803  modaddmodup  12947  modfzo0difsn  12956  modsumfzodifsn  12957  addmodlteq  12959  om2uzlti  12963  fsequb  12988  ssnn0fi  12998  ser1const  13071  expcllem  13085  expeq0  13104  faclbnd  13291  faclbnd6  13300  hashf1rn  13355  hashgadd  13378  hashunx  13387  hashnn0n0nn  13392  hashgt0elex  13401  hashss  13409  hashfzp1  13430  hashxp  13433  hashimarni  13440  seqcoll  13460  hash2exprb  13465  hashge2el2difr  13475  elss2prb  13481  brfi1indlem  13490  fi1uzind  13491  brfi1indALT  13494  lswlgt0cl  13563  ccat1st1st  13622  swrdnd  13652  swrd0  13654  swrdsbslen  13668  swrdspsleq  13669  2swrd1eqwrdeq  13674  swrdswrdlem  13679  swrdswrd  13680  wrd2ind  13697  swrdccatfn  13702  swrdccatin1  13703  swrdccatin12lem2a  13705  swrdccatin2  13707  swrdccatin12lem2  13709  swrdccatin12lem3  13710  swrdccatin12  13711  swrdccat3  13712  swrdccat  13713  swrdccat3blem  13715  repswswrd  13751  repswrevw  13753  cshwmodn  13761  cshwsublen  13762  cshwidxmod  13769  cshwidxmodr  13770  cshf1  13776  2cshw  13779  cshweqrep  13787  cshw1  13788  2cshwcshw  13791  cshwcshid  13793  cshwcsh2id  13794  wrdlen2i  13907  2swrd2eqwrdeq  13917  wwlktovfo  13922  relexpsucnnl  13991  rtrclreclem3  14019  rtrclreclem4  14020  relexpindlem  14022  cjexp  14109  absexp  14263  r19.29uz  14309  caubnd  14317  sqreu  14319  climshft  14526  climub  14611  climserle  14612  sumss  14674  sumss2  14676  modfsummods  14744  o1fsum  14764  binom  14781  bcxmas  14786  climcndslem1  14800  climcndslem2  14801  pwm1geoser  14819  cvgrat  14834  clim2prod  14839  prodfn0  14845  prodfrec  14846  ntrivcvgfvn0  14850  fprodn0  14928  fprodmodd  14947  fprodefsum  15044  demoivreALT  15150  znnenlem  15159  ruclem8  15185  dvdsaddre2b  15251  dvdsdivcl  15260  dvdsfac  15270  oddnn02np1  15294  oddge22np1  15295  evennn02n  15296  evennn2n  15297  m1exp1  15315  nn0o  15321  pwp1fsum  15336  flodddiv4  15359  smu01lem  15429  dvdslegcd  15448  gcdneg  15465  dfgcd2  15485  gcdmultiple  15491  seq1st  15506  alginv  15510  lcmf  15568  lcmftp  15571  lcmfunsnlem2lem2  15574  lcmfunsnlem  15576  lcmfun  15580  ncoprmgcdne1b  15585  coprmproddvdslem  15598  coprmproddvds  15599  cncongr1  15603  prmdvdsexp  15649  prmndvdsfaclt  15657  ncoprmlnprm  15658  fvprmselgcd1  15971  prmgaplem6  15982  prmgaplem7  15983  prmgaplem8  15984  cshwshashlem1  16024  setsstruct2  16118  setsstruct  16120  inveq  16655  catsubcat  16720  initoeu2lem0  16884  initoeu2lem1  16885  funcestrcsetclem8  17008  funcestrcsetclem9  17009  fthestrcsetc  17011  fullestrcsetc  17012  funcsetcestrclem9  17024  fthsetcestrc  17026  fullsetcestrc  17027  lubss  17342  lubel  17343  issstrmgm  17473  mgmb1mgm1  17475  frmdgsum  17620  mgm2nsgrplem3  17628  dfgrp2  17668  gaass  17950  gsumwrev  18016  symgextf1lem  18060  symgextf1  18061  fvcosymgeq  18069  gsmsymgreq  18072  symgfixelsi  18075  pmtrprfv3  18094  symggen  18110  pmtrprfval  18127  gsumzres  18530  gsumzunsnd  18575  srgmulgass  18751  srgbinom  18765  lmodvsmmulgdi  19120  lmodfopnelem1  19121  rmodislmodlem  19152  0ringnnzr  19491  assamulgscm  19572  gsumply1subr  19826  gsummoncoe1  19896  pf1ind  19941  cnfldmulg  20000  cnfldexp  20001  psgndiflemB  20168  matmulcell  20473  mat1dimscm  20503  dmatmul  20525  dmatscmcl  20531  scmataddcl  20544  scmatsubcl  20545  scmatsgrp1  20550  mavmulsolcl  20579  ma1repveval  20599  1marepvmarrepid  20603  symgmatr01lem  20681  slesolvec  20707  cramerimplem2  20712  decpmatmullem  20798  pm2mpf1  20826  mp2pm2mplem4  20836  monmat2matmon  20851  chpscmat  20869  chpscmatgsumbin  20871  fvmptnn04ifb  20878  chfacfscmul0  20885  chfacfscmulgsum  20887  chfacfpmmul0  20889  chfacfpmmulgsum  20891  cpmadugsumlemF  20903  clsss  21080  ntrss  21081  restntr  21208  cmpsublem  21424  cmpsub  21425  2ndcrest  21479  txindislem  21658  t0kq  21843  filufint  21945  fbflim2  22002  flftg  22021  alexsubALTlem4  22075  cnextfvval  22090  tmdmulg  22117  ustuqtop4  22269  xmettri2  22366  mettri  22378  metss  22534  tngngp3  22681  clmvscom  23110  lmmbr  23276  caublcls  23327  lmcau  23331  ovolunlem1a  23484  nulmbl2  23524  voliunlem1  23538  iunmbl  23541  volsup  23544  dvlip  23975  dvfsumle  24003  degltlem1  24051  ply1divex  24115  plyco  24216  dgrnznn  24222  dvnply2  24261  plydivex  24271  aannenlem2  24303  aaliou3lem2  24317  ulmcau  24368  zabsle1  25241  gausslemma2dlem1a  25310  gausslemma2dlem2  25312  gausslemma2dlem3  25313  gausslemma2dlem4  25314  2lgslem1a1  25334  dchrisumlem1  25398  dchrisumlem2  25399  dchrisumlem3  25400  qabvle  25534  ostthlem2  25537  ostth2lem2  25543  axeuclidlem  26062  incistruhgr  26194  umgredgprv  26222  umgrpredgv  26255  usgredgprvALT  26307  uhgr2edg  26320  usgredg2vlem2  26338  lfuhgr1v0e  26366  subgrfun  26393  umgrres1lem  26422  upgrres1  26425  fusgrfis  26442  uhgrnbgr0nb  26470  nbgr1vtx  26474  nb3grprlem1  26501  uvtx01vtx  26521  uvtxa01vtx0OLD  26523  fusgrn0degnn0  26626  vtxdginducedm1lem4  26669  finsumvtxdg2size  26677  upgrewlkle2  26733  wlkl1loop  26765  wlkres  26798  lfgrwlknloop  26817  pthdadjvtx  26857  upgr2pthnlp  26859  upgrwlkdvdelem  26863  upgrwlkdvde  26864  uhgrwkspthlem2  26881  usgr2trlspth  26888  usgr2pth  26891  pthdlem2lem  26894  lfgrn1cycl  26929  uspgrn2crct  26932  crctcshwlkn0lem3  26936  crctcshwlkn0lem4  26937  crctcshwlkn0lem5  26938  iswspthsnon  26982  wlkiswwlks1  26997  wlklnwwlkln1  26998  wlkiswwlks2  27005  wlkiswwlksupgr2  27007  wlklnwwlkln2lem  27012  wwlksnred  27031  wwlksnext  27032  wwlksnredwwlkn  27034  wwlksnredwwlkn0  27035  wwlksnextfun  27037  wwlksnextinj  27038  wwlksnextsur  27039  wspthsnonn0vne  27058  wspn0  27065  wwlks2onv  27094  elwwlks2  27109  elwspths2spth  27110  rusgrnumwwlk  27118  clwwlknclwwlkdifsOLD  27123  clwwlkccatlem  27133  clwlkclwwlklem2a1  27136  clwlkclwwlklem2fv2  27140  clwlkclwwlklem2a4  27141  clwlkclwwlklem2a  27142  clwlkclwwlklem2  27144  clwlkclwwlkf1lem3  27150  clwwisshclwwslem  27158  clwwisshclwwsn  27160  erclwwlktr  27166  isclwwlknx  27185  clwwlkinwwlk  27190  clwwlkel  27196  clwwlkf  27197  clwwlkf1  27199  clwwlkfo  27200  clwwlkext2edg  27207  wwlksext2clwwlk  27208  wwlksext2clwwlkOLD  27209  wwlksubclwwlk  27210  clwwlknscsh  27214  erclwwlkntr  27223  eleclclwwlkn  27228  hashecclwwlkn1  27229  umgrhashecclwwlk  27230  clwlksfclwwlkOLD  27237  clwlksfoclwwlkOLD  27238  clwwlknon0  27261  clwwlknonel  27263  clwwlknon1  27266  clwwlknonwwlknonb  27275  clwwlknonwwlknonbOLD  27276  clwwlknonex2lem2  27278  clwwlknun  27282  clwwlkvbij  27283  clwwlkvbijOLD  27284  clwwlknunOLD  27286  upgr3v3e3cycl  27353  uhgr3cyclex  27355  upgr4cycl4dv4e  27358  eulerpath  27414  eucrctshift  27416  eucrct2eupth  27418  1to2vfriswmgr  27454  1to3vfriswmgr  27455  3cyclfrgrrn1  27460  4cycl2vnunb  27465  frgrwopreglem2  27488  frgrwopreglem3  27489  frgrwopreglem5ALT  27497  fusgr2wsp2nb  27509  numclwwlk2lem1lemOLD  27520  2clwwlk2clwwlklem  27524  2clwwlk2clwwlk  27528  numclwlk1lem2f1  27537  numclwlk1lem2fo  27538  numclwwlk1  27541  clwwlknonclwlknonf1o  27543  dlwwlknondlwlknonf1o  27547  numclwlk1  27553  numclwlk2lem2f  27559  numclwlk2lem2f1o  27561  numclwlk2lem2fOLD  27566  numclwlk2lem2f1oOLD  27568  numclwwlk5  27577  frgrreg  27583  frgrregord013  27584  friendship  27588  nsnlplig  27665  nsnlpligALT  27666  isgrpo  27681  vcdi  27750  vcdir  27751  vcass  27752  nmosetre  27949  hlim2  28379  shscli  28506  chintcli  28520  dfch2  28596  spansncvi  28841  nmopsetretALT  29052  nmfnsetre  29066  lnopl  29103  lnfnl  29120  pjss2coi  29353  pjorthcoi  29358  pjscji  29359  pjssdif2i  29363  pjclem4a  29387  pj3lem1  29395  strlem5  29444  hstrlem5  29452  cvmdi  29513  mdslmd3i  29521  atcv1  29569  atcvat4i  29586  cdj3lem2a  29625  cdj3lem3a  29628  iuninc  29707  disji2f  29718  disjif2  29722  fmptcof2  29787  nnindd  29896  xrsmulgzz  30008  ofldchr  30144  esumfzf  30461  issgon  30516  voliune  30622  volfiniune  30623  rrvsum  30846  bnj228  31131  bnj1294  31216  bnj229  31282  bnj607  31314  bnj908  31329  bnj953  31337  bnj1118  31380  bnj1174  31399  bnj1388  31429  cvmliftlem15  31608  iprodefisumlem  31954  faclimlem1  31957  dfon2lem6  32019  tfisg  32042  poseq  32080  frrlem5c  32113  noprefixmo  32175  nosupbnd1lem5  32185  nocvxminlem  32220  nocvxmin  32221  slerec  32250  idinside  32518  nn0prpw  32645  onsucconni  32763  axc11n11r  33001  bj-finsumval0  33476  exlimim  33518  exellim  33521  icoreclin  33534  wl-spae  33637  wl-aleq  33653  fin2so  33727  matunitlindf  33738  poimirlem4  33744  poimirlem26  33766  itg2addnclem  33792  upixp  33855  welb  33862  sdclem2  33869  metf1o  33882  sstotbnd3  33906  isbndx  33912  ismtycnv  33932  heiborlem4  33944  bfplem1  33952  opidonOLD  33982  grpomndo  34005  ax12eq  34748  ax12el  34749  cvrat4  35250  mzpexpmpt  37828  diophren  37897  expmordi  38032  rmxypos  38034  jm2.17a  38047  jm2.17b  38048  rmygeid  38051  jm2.18  38075  jm2.25  38086  jm2.15nn0  38090  jm2.16nn0  38091  pwslnm  38184  isnumbasgrplem1  38191  dgraalem  38235  relexpiidm  38516  relexpmulnn  38521  relexpmulg  38522  relexp01min  38525  relexp0a  38528  relexpxpmin  38529  clsk1indlem3  38861  dvgrat  39031  radcnvrat  39033  sspwimpcf  39673  sspwimpcfVD  39674  e2ebindALT  39682  2reurex  41705  2reu1  41710  eu2ndop1stv  41726  afvfv0bi  41756  afveu  41757  afvres  41776  aovmpt4g  41805  ndmaovass  41810  ndmaovdistr  41811  imarnf1pr  41827  nltle2tri  41851  fzopredsuc  41861  subsubelfzo0  41864  fzoopth  41865  2ffzoeq  41866  smonoord  41869  iccpartres  41882  iccpartiltu  41886  iccpartigtl  41887  iccpartgt  41891  icceuelpartlem  41899  fargshiftf1  41905  pfxsuff1eqwrdeq  41935  pfxccatin12lem2  41952  pfxccatin12  41953  pfxccat3  41954  pfxccat3a  41957  cshword2  41965  goldbachth  41987  fmtnoprmfac1  42005  fmtnoprmfac2  42007  prmdvdsfmtnof1lem2  42025  lighneallem2  42051  lighneallem4  42055  even3prm2  42156  gbegt5  42177  sbgoldbwt  42193  sbgoldbm  42200  nnsum3primesgbe  42208  wtgoldbnnsum4prm  42218  bgoldbnnsum3prm  42220  bgoldbtbndlem2  42222  bgoldbtbndlem3  42223  bgoldbtbndlem4  42224  bgoldbtbnd  42225  upgrwlkupwlk  42249  elsprel  42253  sprsymrelfo  42275  uspgropssxp  42280  uspgrsprfo  42284  mgmpropd  42303  isassintop  42374  lidldomn1  42449  lidlmmgm  42453  2zlidl  42462  2zrngamgm  42467  2zrngmmgm  42474  rnghmsscmap  42502  rnghmsubcsetclem2  42504  rngcinv  42509  rngccatidALTV  42517  rngcinvALTV  42521  funcrngcsetc  42526  funcrngcsetcALT  42527  rhmsscmap  42548  rhmsubcsetclem2  42550  rhmsubcrngclem2  42556  ringcinv  42560  funcringcsetc  42563  funcringcsetcALTV2lem9  42572  ringccatidALTV  42580  ringcinvALTV  42584  srhmsubc  42604  rhmsubclem4  42617  srhmsubcALTV  42622  rhmsubcALTVlem4  42635  gsumpr  42667  lmodvsmdi  42691  ply1mulgsumlem1  42702  ply1mulgsumlem2  42703  lincdifsn  42741  lincsumcl  42748  lincscmcl  42749  lincext3  42773  lindslinindsimp1  42774  lindslinindsimp2lem5  42779  snlindsntor  42788  lincresunit2  42795  lincresunit3lem2  42797  lincresunit3  42798  zgtp1leeq  42839  m1modmmod  42844  elbigo2  42874  fllog2  42890  digexp  42929  dig1  42930  nn0sumshdiglemA  42941  nn0sumshdiglemB  42942
  Copyright terms: Public domain W3C validator