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

Theorem com12 32
Description: Inference that swaps (commutes) antecedents in an implication. Inference associated with pm2.04 90. Its associated inference is mpi 20. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)
Hypothesis
Ref Expression
com12.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
com12 (𝜓 → (𝜑𝜒))

Proof of Theorem com12
StepHypRef Expression
1 id 22 . 2 (𝜓𝜓)
2 com12.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5com 31 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syl11  33  syl5  34  syl6com  37  mpcom  38  syli  39  syl2imc  41  pm2.27  42  syldc  48  pm2.43b  55  syl9r  78  com3r  87  pm2.86i  110  pm2.24  122  con3rr3  153  expt  170  jad  176  pm2.61  184  syl5ibcom  237  syl5ibrcom  239  pm5.501  358  impcom  398  impd  400  impcomdOLD  402  expcom  404  expdcom  405  expdOLD  407  simplbi2com  498  imdistanri  565  jaod  848  orel1  875  pm2.62  886  pm2.75  920  pm2.64  928  ccased  1022  dedlem0b  1028  3impd  1410  3expd  1415  mp3an1i  1527  minimp  1679  meredith  1685  19.35  1924  speimfw  2007  sbequ2  2013  equtrr  2069  equeucl  2071  sb56  2248  exsb  2327  nfeqf2OLD  2340  cbv1  2364  ax12b  2390  axc11n  2392  dvelimdf  2415  equvel  2422  sbied  2485  exsbOLD  2548  mo3  2580  mo3OLD  2581  dfmo  2615  euexOLD  2629  exmoeuOLD  2632  2mo  2678  2eu6  2687  exists2  2693  exists2OLD  2694  rexlimdv  3212  r19.12  3248  r19.12OLD  3249  2gencl  3438  3gencl  3439  rspccv  3508  ceqex  3536  mob  3600  euind  3605  reuind  3628  sseq2  3846  nelss  3883  reupick2  4139  rspn0  4162  disjeq0  4248  uneqdifeq  4281  ssprsseq  4587  preq12b  4610  prel12OLD  4611  prnebg  4617  prel12g  4627  3elpr2eq  4670  iinss2  4805  trintss  5005  dtru  5082  reusv2lem1  5110  alxfr  5119  ralxfrALT  5127  sspwb  5149  copsexg  5187  snopeqop  5202  propeqop  5204  opthhausdorff  5214  opthhausdorff0  5215  pocl  5281  pofun  5291  solin  5298  frss  5322  2optocl  5444  3optocl  5445  ssrel  5455  ssrel2  5457  ssrelrel  5467  relop  5518  dfres3  5647  asymref2  5768  xpidtr  5773  trin2  5774  poltletr  5783  xp11  5823  relcnvtr  5909  tz7.7  6002  ordtr2  6020  suc11  6079  iotaval  6110  funmo  6151  fundif  6183  fss  6304  f0dom0  6339  fv3  6464  tz6.12i  6472  mpteqb  6560  fveqdmss  6618  eldmrexrnb  6630  funopsn  6679  funsndifnop  6682  tpres  6738  funfvima  6764  fvclss  6772  f1veqaeq  6786  isoselem  6863  oprabv  6980  ovg  7076  elovmpt3rab1  7170  sorpsscmpl  7225  iunpw  7256  ordom  7352  limom  7358  peano5  7367  fornex  7414  bropopvvv  7536  bropfvvvvlem  7537  f1o2ndf1  7566  poxp  7570  soxp  7571  suppimacnv  7587  ressuppss  7595  ressuppssdif  7597  tposfn2  7656  wfr3g  7695  onnseq  7724  smoel  7740  smogt  7747  smoiso2  7749  tfr3  7778  tz7.48-2  7820  tz7.48-3  7822  tz7.49  7823  oecl  7901  oaordex  7922  oalimcl  7924  oaass  7925  omordi  7930  omlimcl  7942  odi  7943  omeulem1  7946  oen0  7950  nnawordi  7985  nnaass  7986  nnmordi  7995  omabs  8011  omsmolem  8017  iiner  8102  2ecoptocl  8121  3ecoptocl  8122  undifixp  8230  xpdom2  8343  xpf1o  8410  infensuc  8426  php  8432  onomeneq  8438  isinf  8461  findcard2  8488  unblem2  8501  infssuni  8545  finsschain  8561  fsuppunfi  8583  fsuppunbi  8584  marypha1  8628  hartogs  8738  card2on  8748  card2inf  8749  xpwdomg  8779  elirrv  8790  en3lp  8806  preleqg  8807  inf3lem1  8822  inf3lem2  8823  inf3lem3  8824  inf3lem5  8826  noinfep  8854  trcl  8901  tcel  8918  rankonidlem  8988  scottex  9045  djuunxp  9080  eldju2ndl  9083  updjud  9093  dif1card  9166  fodomnum  9213  cardaleph  9245  kmlem9  9315  kmlem13  9319  cflim2  9420  cfsmolem  9427  infpssrlem3  9462  isfin7-2  9553  fin1a2lem6  9562  fin1a2lem12  9568  domtriomlem  9599  axdc3lem4  9610  axdc4lem  9612  zorn2lem3  9655  zorn2lem4  9656  zorn2lem5  9657  zorn2lem7  9659  zornn0g  9662  axdclem2  9677  ondomon  9720  alephval2  9729  cfpwsdom  9741  wuncval2  9904  grupr  9954  gruiun  9956  ingru  9972  grothomex  9986  indpi  10064  nqereu  10086  prlem934  10190  reclem2pr  10205  mulgt0sr  10262  supsrlem  10268  dedekind  10539  lemul1a  11231  squeeze0  11280  peano5nni  11377  nnunb  11638  nn0lt2  11792  nn0le2is012  11793  fzind  11827  nn0ind-raph  11829  zindd  11830  eluzadd  12021  uzin  12026  nn01to3  12088  xnn0xadd0  12389  xmulasslem  12427  icoshft  12609  fzen  12675  uzsubsubfz  12680  elfz0ubfz0  12762  elfz0fzfz0  12763  fz0fzelfz0  12764  elfzmlbp  12769  elfzodifsumelfzo  12853  ssfzo12bi  12882  elfzonelfzo  12889  elfznelfzo  12892  injresinjlem  12907  injresinj  12908  modfzo0difsn  13061  modsumfzodifsn  13062  addmodlteq  13064  ssnn0fi  13103  fsuppmapnn0fiub0  13111  expcllem  13189  expeq0  13208  mulexp  13217  leexp2r  13236  bernneq  13309  facdiv  13392  hasheqf1oi  13457  hashnn0n0nn  13495  hashss  13511  hashgt12el  13524  hashgt12el2  13525  hashimarni  13542  hashle2pr  13573  pr2pwpr  13575  hashge2el2dif  13576  hashge2el2difr  13577  hashtpg  13581  hashge3el3dif  13582  exprelprel  13585  hash1to3  13587  fundmge2nop0  13588  fi1uzind  13593  ccatsymb  13672  swrdnd  13749  swrdnd2  13750  swrdnnn0nd  13751  swrdnd0  13752  pfxnd0  13797  swrdswrdlem  13813  swrdswrd  13814  swrdccatin1  13851  swrdccatin12lem2a  13853  pfxccatin12lem1  13854  swrdccatin12lem2bOLD  13855  swrdccatin2  13856  pfxccatin12lem2  13858  swrdccatin12lem2OLD  13859  swrdccatin12lem3  13860  pfxccat3  13863  swrdccat3OLD  13864  swrdccat  13865  swrdccatOLD  13866  swrdccat3blem  13871  repsdf2  13924  repswswrd  13930  cshwidxmod  13954  cshwidx0  13957  cshf1  13961  2cshw  13964  cshweqrep  13972  cshw1  13973  cshwsexa  13975  2cshwcshw  13976  scshwfzeqfzo  13977  cshwcsh2id  13979  wwlktovfo  14110  relexpaddg  14200  iseraltlem2  14821  modfsummods  14929  clim2prod  15023  prodfn0  15029  prodfrec  15030  prodmo  15069  fprodabs  15107  binomfallfac  15174  fprodefsum  15227  dvdsaddre2b  15436  addmodlteqALT  15454  oddge22np1  15477  nn0enne  15507  nn0o1gt2  15511  sumeven  15517  sumodd  15518  dvdslegcd  15632  gcdneg  15649  dfgcd2  15669  rplpwr  15682  lcmf  15752  lcmftp  15755  lcmfunsnlem2lem1  15757  lcmfunsnlem2  15759  lcmfdvdsb  15762  coprmdvds1  15771  qredeq  15776  coprmprod  15780  coprmproddvdslem  15781  cncongr1  15786  cncongr2  15787  prm2orodd  15809  nnnn0modprm0  15915  prm23lt5  15923  prm23ge5  15924  dvdsprmpweqnn  15993  dvdsprmpweqle  15994  oddprmdvds  16011  prmpwdvds  16012  prmreclem4  16027  ramcl  16137  prmgaplem6  16164  prmgaplem7  16165  prmgaplem8  16166  cshwshashlem1  16201  cshwshashlem2  16202  cshwshashlem3  16203  cshwrepswhash1  16208  setsn0fun  16292  setsstruct2  16293  imasleval  16587  mreiincl  16642  mreexexd  16694  inveq  16819  cicsym  16849  cictr  16850  initoid  17040  termoid  17041  initoeu2lem0  17048  initoeu2lem1  17049  initoeu2lem2  17050  initoeu2  17051  fthestrcsetc  17176  fthsetcestrc  17191  drsdirfi  17324  isnmgm  17632  sgrpass  17676  mgm2nsgrplem3  17794  dfgrp3lem  17900  symg2bas  18201  symgfix2  18219  symgextf1  18224  gsmsymgrfix  18231  pmtrprfv3  18257  psgnunilem4  18301  efgi2  18522  lmodvsmmulgdi  19290  0ringnnzr  19666  mpfrcl  19914  gsummoncoe1  20070  psgndiflemB  20342  psgndiflemA  20343  elfrlmbasn0  20506  lmictra  20588  mamufacex  20599  matecl  20635  dmatelnd  20707  dmatscmcl  20714  scmateALT  20723  scmatsgrp1  20733  scmatf1  20742  mavmulsolcl  20762  cramerimplem1  20895  cramerimplem1OLD  20896  cramerimplem2  20897  pmatcollpw3fi1  21000  mp2pm2mplem4  21021  pm2mpfo  21026  chmaidscmat  21060  fvmptnn04ifb  21063  chfacfscmul0  21070  chfacfpmmul0  21074  cayhamlem1  21078  cayhamlem3  21099  cayleyhamilton1  21104  fiinopn  21113  toprntopon  21137  tgcl  21181  distop  21207  isclo2  21300  iscldtop  21307  ssnei2  21328  opnnei  21332  pnfnei  21432  mnfnei  21433  tgcnp  21465  cnpnei  21476  1stcelcls  21673  txcnpi  21820  cnmptcom  21890  fbfinnfr  22053  isfildlem  22069  snfil  22076  fbunfip  22081  fgcl  22090  elfm2  22160  fmco  22173  fbflim2  22189  cnpflf2  22212  flimfcls  22238  tmdgsum  22307  neibl  22714  tngngpim  22871  cphsscph  23457  fgcfil  23477  caubl  23514  volsuplem  23759  ellimc3  24080  dvnadd  24129  dvnres  24131  cpnord  24135  dvnfre  24152  ply1divex  24333  cxpmul2  24872  zabsle1  25473  gausslemma2dlem0i  25541  gausslemma2dlem1a  25542  gausslemma2dlem3  25545  lgsquad2lem2  25562  2lgs  25584  qabvexp  25767  axcontlem4  26316  umgredgprv  26455  umgrnloop  26456  upgrpredgv  26488  upgredgpr  26491  edglnl  26492  usgredgprvALT  26541  usgrnloopALT  26549  usgredg2v  26573  fusgrfis  26677  nbuhgr2vtx1edgblem  26698  nb3grprlem1  26728  cusgrsize2inds  26801  cusgrfi  26806  fusgrn0degnn0  26847  uspgrloopvtxel  26864  vtxdginducedm1lem4  26890  uhgr0edg0rgrb  26922  wlkl1loop  26985  wlk1walk  26986  upgriswlk  26988  upgrwlkvtxedg  26992  uspgr2wlkeq  26993  wlkv0  26998  wlklenvclwlk  27002  wlksoneq1eq2  27011  wlkon2n0  27013  wlkreslem  27018  wlkres  27019  wlkreslemOLD  27020  wlkresOLD  27021  lfgrwlkprop  27038  pthdivtx  27081  2pthnloop  27083  spthonepeq  27104  uhgrwkspthlem2  27106  uhgrwkspth  27107  usgr2wlkneq  27108  usgr2trlncl  27112  usgr2pthlem  27115  usgr2pth  27116  cyclnspth  27152  lfgrn1cycl  27154  usgr2trlncrct  27155  uspgrn2crct  27157  crctcshwlkn0lem3  27161  crctcshwlkn0lem5  27163  wwlknp  27192  wspthneq1eq2  27209  0enwwlksnge1  27213  wlklnwwlkln1  27217  wlkiswwlks2  27224  wlkiswwlksupgr2  27226  wlklnwwlkln2lem  27232  wwlksnred  27252  wwlksnredOLD  27253  wwlksnext  27254  wwlksnextbi  27255  wwlksnextbiOLD  27256  wwlksnredwwlkn0  27259  wwlksnredwwlkn0OLD  27260  wwlksnextwrd  27261  wwlksnextinj  27263  wwlksnextwrdOLD  27266  wwlksnextinjOLD  27268  wwlksnextproplem3  27287  wwlksnextproplem3OLD  27288  wwlksnextprop  27289  wwlksnextpropOLD  27290  wspthsnwspthsnon  27296  wspthsnonn0vne  27297  2pthon3v  27323  umgr2adedgwlkonALT  27327  umgr2wlk  27329  umgr2wlkon  27330  umgrwwlks2on  27337  elwspths2on  27340  usgr2wspthons3  27344  elwwlks2  27346  rusgrnumwwlk  27356  clwwlkccatlem  27369  clwwlkccat  27370  clwlkclwwlklem2a4  27377  clwlkclwwlklem2a  27378  clwlkclwwlklem2  27380  clwlkclwwlkf1lem3  27389  clwlkclwwlkf1lem3OLD  27390  erclwwlkeqlen  27408  clwwlknwwlksn  27427  loopclwwlkn1b  27432  clwwlkf1OLD  27440  clwwlkf1  27445  wwlksext2clwwlk  27454  eleclclwwlknlem2  27459  umgr2cwwk2dif  27462  eleclclwwlkn  27474  hashecclwwlkn1  27475  umgrhashecclwwlk  27476  clwwlknonwwlknonb  27508  clwwlknonex2lem2  27510  clwwlknonex2  27511  1pthon2v  27556  upgr3v3e3cycl  27583  uhgr3cyclexlem  27584  uhgr3cyclex  27585  eupth2lem3lem4  27635  frgr3vlem1  27681  frgr3vlem2  27682  3vfriswmgrlem  27685  3vfriswmgr  27686  3cyclfrgrrn1  27693  n4cyclfrgr  27699  frgrncvvdeqlem3  27709  frgrncvvdeqlem6  27712  frgrncvvdeqlem7  27713  frgrncvvdeqlem8  27714  frgrwopreglem4a  27718  frgrwopreglem3  27722  frgrwopreg1  27726  frgrwopreg2  27727  frgrwopreglem5lem  27728  frgrwopreglem5ALT  27730  frgrwopreg  27731  fusgr2wsp2nb  27742  2wspmdisj  27745  numclwwlk1lem2foa  27769  numclwwlk1lem2foaOLD  27770  numclwwlk1lem2f1  27773  numclwwlk1lem2fo  27774  numclwwlk1lem2f1OLD  27778  numclwwlk1lem2foOLD  27779  numclwwlk1  27784  wlkl0  27795  numclwwlk2lem1  27804  numclwlk2lem2f  27805  numclwlk2lem2f1o  27807  numclwlk2lem2fOLD  27808  numclwlk2lem2f1oOLD  27810  frgrreg  27826  frgrregord013  27827  frgrregord13  27828  friendshipgt3  27830  friendship  27831  eulplig  27912  ipassi  28268  ubthlem2  28299  isch3  28670  shintcli  28760  shmodsi  28820  spansncvi  29083  hoaddsub  29247  eigorthi  29268  pjss2coi  29595  pjnormssi  29599  pj3cor1i  29640  strb  29689  dmdmd  29731  mdsl0  29741  csmdsymi  29765  chrelat2i  29796  mdsymlem3  29836  mdsymlem6  29839  sumdmdlem2  29850  ssrelf  29990  cvmlift2lem1  31883  mrsubvrs  32018  mclsax  32065  3ccased  32197  dfon2lem3  32278  rdgprc  32288  trpredmintr  32319  trpredrec  32326  frr3g  32368  sltval2  32398  nolt02o  32434  sslttr  32503  scutun12  32506  cgrextend  32704  btwndiff  32723  btwnconn1lem12  32794  brsegle  32804  broutsideof2  32818  funray  32836  elicc3  32900  nn0prpwlem  32905  nn0prpw  32906  fnessref  32940  neibastop2lem  32943  filnetlem4  32964  meran1  32993  waj-ax  32996  arg-ax  32998  bj-con2com  33126  bj-axdd2  33155  bj-exalimi  33191  bj-cbvalimt  33197  bj-ssbequ2  33233  bj-ssbequ1  33234  bj-ssbid1ALT  33238  bj-sb  33266  bj-cbv1v  33316  bj-dtru  33373  bj-mo3OLD  33407  bj-snsetex  33523  bj-restpw  33618  bj-finsumval0  33749  mptsnunlem  33781  icoreclin  33800  relowlpssretop  33807  wl-dral1d  33912  wl-exeq  33915  wl-lem-exsb  33942  poimirlem29  34064  poimirlem32  34067  fdc  34165  seqpo  34167  incsequz  34168  isismty  34224  ismtybndlem  34229  heibor1lem  34232  ismgmOLD  34273  isexid2  34278  ghomco  34314  pridlc  34494  relcnveq3  34720  elrelscnveq3  34869  cdleme18d  36449  tendovalco  36919  cdlemn11pre  37364  dihord2pre  37379  incssnn0  38234  fphpd  38340  jm2.19lem3  38517  setindtr  38550  islssfg2  38600  mpaaeu  38679  refimssco  38870  iunrelexpmin1  38957  iunrelexpmin2  38961  trclimalb2  38975  clsk1indlem3  39297  syldbl2  39424  nzss  39472  sb5ALT  39685  truniALT  39701  ee223  39803  3orbi123VD  40019  sbc3orgVD  40020  exbirVD  40022  exbiriVD  40023  sbcim2gVD  40044  trsbcVD  40046  truniALTVD  40047  onfrALTlem3VD  40056  onfrALTlem2VD  40058  csbrngVD  40065  19.41rgVD  40071  ax6e2eqVD  40076  ax6e2ndeqVD  40078  2uasbanhVD  40080  sb5ALTVD  40082  vk15.4jVD  40083  infxrunb3rnmpt  40561  stoweidlem26  41170  hirstL-ax3  41986  rexsb  42127  rexrsb  42128  euoreqb  42141  2reu1  42147  2reu8i  42154  afvres  42213  tz6.12-afv  42214  afvco2  42217  afv2orxorb  42269  afv2res  42280  tz6.12-afv2  42281  tz6.12i-afv2  42284  dfatcolem  42296  zm1nn  42344  fzoopth  42369  2ffzoeq  42370  smonoord  42373  iccpartiltu  42390  iccpartlt  42392  iccpartltu  42393  iccpartgtl  42394  iccpartgt  42395  iccpartleu  42396  iccpartgel  42397  icceuelpart  42404  iccpartnel  42406  lswn0  42412  prsprel  42426  sprsymrelfvlem  42429  sprsymrelf1lem  42430  sprsymrelfolem2  42432  prproropf1olem4  42445  paireqne  42450  prprelb  42455  goldbachth  42480  odz2prm2pw  42496  fmtno4prmfac  42505  fmtno4prmfac193  42506  prmdvdsfmtnof1lem2  42518  2pwp1prmfmtno  42525  lighneallem2  42544  lighneallem4b  42547  lighneallem4  42548  requad2  42561  odd2prm2  42652  mogoldbblem  42654  gbepos  42671  gbowgt5  42675  gbowge7  42676  stgoldbwt  42689  sbgoldbwt  42690  sbgoldbst  42691  sbgoldbaltlem1  42692  sbgoldbalt  42694  sbgoldbo  42700  nnsum3primesle9  42707  nnsum4primesodd  42709  nnsum4primesoddALTV  42710  nnsum4primeseven  42713  nnsum4primesevenALTV  42714  bgoldbtbndlem1  42718  bgoldbtbndlem2  42719  bgoldbtbndlem3  42720  bgoldbtbnd  42722  isomuspgrlem1  42740  upgrwlkupwlk  42763  uspgrsprf1  42770  mgmhmlin  42801  issubmgm2  42805  lmod0rng  42883  lidldomn1  42936  lidlmmgm  42940  rnghmsscmap  42989  rnghmsubcsetclem2  42991  rngcinv  42996  rngccatidALTV  43004  rngcinvALTV  43008  funcrngcsetc  43013  funcrngcsetcALT  43014  rhmsscmap  43035  rhmsubcsetclem2  43037  rhmsubcrngclem2  43043  ringcinv  43047  ringcbasbas  43049  funcringcsetc  43050  funcringcsetcALTV2lem9  43059  ringccatidALTV  43067  ringcinvALTV  43071  ringcbasbasALTV  43073  rhmsubclem4  43104  rhmsubcALTVlem4  43122  ztprmneprm  43140  pgrpgt2nabl  43162  lmodvsmdi  43178  ply1mulgsumlem2  43190  lincsumcl  43235  ellcoellss  43239  linindslinci  43252  islinindfis  43253  lincext3  43260  lindslinindimp2lem4  43265  lindslinindsimp2lem5  43266  lindslinindsimp2  43267  lindsrng01  43272  ldepspr  43277  lincresunit3lem1  43283  elfzolborelfzop1  43324  dignn0ldlem  43411  nn0sumshdiglem1  43430  rrx2xpref1o  43454  rrx2plord2  43458  rrx2plordisom  43459  line2ylem  43487  line2xlem  43489  line2y  43491  itschlc0xyqsol1  43502  inlinecirc02plem  43522  tfis2d  43532  onsetrec  43559
  Copyright terms: Public domain W3C validator