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

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2		com12.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5com 31	1 ⊢ (𝜓 → (𝜑 → 𝜒))

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  124  con3rr3  155  expt  177  jad  187  pm2.61  192  syl5ibcom  245  syl5ibrcom  247  pm5.501  366  impcom  407  impd  410  expcom  413  expdcom  414  simplbi2com  502  imdistanri  569  syldbl2  841  jaod  859  orel1  888  pm2.62  899  pm2.75  933  pm2.64  943  ccased  1038  dedlem0b  1044  3impd  1347  3expd  1352  mp3an1i  1453  minimp  1617  meredith  1637  19.35  1874  speimfw  1960  equtrr  2018  equeucl  2020  ax12ev2  2177  sbiedw  2314  cbv1v  2336  exsb  2359  cbv1  2404  ax12b  2426  axc11n  2428  dvelimdf  2451  equvel  2458  dfsb1  2483  sbied  2505  dfmoeu  2533  mo3  2561  mo4  2563  2mo  2645  2eu6  2654  exists2  2659  pm2.61dne  3025  rexlimdv  3150  r19.21v  3177  r19.12  3311  r19.12OLD  3312  2gencl  3521  3gencl  3522  vtocl2ga  3577  vtocl2gaf  3578  vtocl3gaf  3580  vtocl3ga  3582  vtocl4ga  3585  rspccv  3618  ceqex  3651  mob  3725  euind  3732  reuind  3761  2reu1  3905  sseq2  4021  nelss  4060  rexdifi  4159  reupick2  4336  disjeq0  4461  uneqdifeq  4498  sspw  4615  ssprsseq  4829  preq12b  4854  prnebg  4860  prel12g  4868  3elpr2eq  4910  iinss2  5061  trintss  5283  dtruALT2  5375  reusv2lem1  5403  alxfr  5412  ralxfrALT  5420  exexneq  5444  dtruOLD  5451  copsexgw  5500  copsexg  5501  snopeqop  5515  propeqop  5516  opthhausdorff  5526  opthhausdorff0  5527  pofun  5614  solin  5622  frss  5652  2optocl  5783  3optocl  5784  ssrel  5794  ssrelOLD  5795  ssrel2  5797  ssrelrel  5808  relop  5863  dfres3  6004  asymref2  6139  xpidtr  6144  trin2  6145  poltletr  6154  xp11  6196  relcnvtrg  6287  reuop  6314  tz7.7  6411  ordtr2  6429  suc11  6492  iotavalOLD  6536  funmoOLD  6583  fundif  6616  fss  6752  f0dom0  6792  fv3  6924  tz6.12i  6934  mpteqb  7034  fveqdmss  7097  eldmrexrnb  7111  funopsn  7167  funsndifnop  7170  tpres  7220  funfvima  7249  fvclss  7260  f1veqaeq  7276  fvf1pr  7326  isoselem  7360  oprabv  7492  ovg  7597  elovmpt3rab1  7692  sorpsscmpl  7752  iunpw  7789  trom  7895  limom  7902  peano5  7915  focdmex  7978  funelss  8070  funeldmdif  8071  bropopvvv  8113  bropfvvvvlem  8114  f1o2ndf1  8145  poxp  8151  soxp  8152  poxp2  8166  frxp2  8167  frxp3  8174  suppimacnv  8197  ressuppss  8206  ressuppssdif  8208  tposfn2  8271  wfr3g  8345  onnseq  8382  smoel  8398  smogt  8405  smoiso2  8407  tfr3  8437  tz7.48-2  8480  tz7.48-3  8482  tz7.49  8483  oecl  8573  oaordex  8594  oalimcl  8596  oaass  8597  omordi  8602  omlimcl  8614  odi  8615  omeulem1  8618  oen0  8622  nnawordi  8657  nnaass  8658  nnmordi  8667  omabs  8687  omsmolem  8693  naddssim  8721  brinxper  8772  iiner  8827  2ecoptocl  8846  3ecoptocl  8847  undifixp  8972  xpdom2  9105  xpf1o  9177  infensuc  9193  findcard2  9202  php  9244  phpOLD  9256  onomeneqOLD  9263  isinf  9293  isinfOLD  9294  unblem2  9326  fodomfir  9365  infssuni  9383  finsschain  9396  fsuppunfi  9425  fsuppunbi  9426  marypha1  9471  hartogs  9581  card2on  9591  card2inf  9592  xpwdomg  9622  elirrv  9633  en3lp  9651  preleqg  9652  inf3lem1  9665  inf3lem2  9666  inf3lem3  9667  inf3lem5  9669  noinfep  9697  ttrclss  9757  ttrclselem2  9763  trcl  9765  tcel  9782  frr3g  9793  rankonidlem  9865  scottex  9922  djuunxp  9958  eldju2ndl  9961  updjud  9971  dif1card  10047  fodomnum  10094  cardaleph  10126  kmlem9  10196  kmlem13  10200  cflim2  10300  cfsmolem  10307  infpssrlem3  10342  isfin7-2  10433  fin1a2lem6  10442  fin1a2lem12  10448  domtriomlem  10479  axdc3lem4  10490  axdc4lem  10492  zorn2lem3  10535  zorn2lem4  10536  zorn2lem5  10537  zorn2lem7  10539  zornn0g  10542  axdclem2  10557  ondomon  10600  alephval2  10609  cfpwsdom  10621  wuncval2  10784  grupr  10834  gruiun  10836  ingru  10852  grothomex  10866  indpi  10944  nqereu  10966  prlem934  11070  reclem2pr  11085  mulgt0sr  11142  supsrlem  11148  dedekind  11421  lemul1a  12118  squeeze0  12168  peano5nni  12266  nnunb  12519  nn0lt2  12678  nn0le2is012  12679  fzind  12713  nn0ind-raph  12715  zindd  12716  eluzaddOLD  12910  uzin  12915  nn01to3  12980  xnn0xadd0  13285  xmulasslem  13323  icoshft  13509  fzen  13577  uzsubsubfz  13582  elfz0ubfz0  13668  elfz0fzfz0  13669  fz0fzelfz0  13670  elfzmlbp  13675  elfzodifsumelfzo  13766  ssfzo12bi  13796  fzoopth  13797  elfzonelfzo  13804  elfznelfzo  13807  injresinjlem  13822  injresinj  13823  modfzo0difsn  13980  modsumfzodifsn  13981  addmodlteq  13983  ssnn0fi  14022  fsuppmapnn0fiub0  14030  expcllem  14109  expeq0  14129  mulexp  14138  leexp2r  14210  bernneq  14264  facdiv  14322  hasheqf1oi  14386  hashnn0n0nn  14426  hashss  14444  hashgt12el  14457  hashgt12el2  14458  hashimarni  14476  hashle2pr  14512  pr2pwpr  14514  hashge2el2dif  14515  hashge2el2difr  14516  hashtpg  14520  hashge3el3dif  14522  exprelprel  14525  hash1to3  14527  hash3tpde  14528  tpfo  14535  fundmge2nop0  14537  fi1uzind  14542  ccatsymb  14616  swrdnd  14688  swrdnd2  14689  swrdnnn0nd  14690  swrdnd0  14691  pfxnd0  14722  swrdswrdlem  14738  swrdswrd  14739  pfxccatin12lem2a  14761  pfxccatin12lem1  14762  swrdccatin2  14763  pfxccatin12lem2  14765  pfxccatin12lem3  14766  pfxccat3  14768  swrdccat  14769  swrdccat3blem  14773  repsdf2  14812  repswswrd  14818  cshwidxmod  14837  cshwidx0  14840  cshf1  14844  cshweqrep  14855  cshw1  14856  cshwsexaOLD  14859  2cshwcshw  14860  scshwfzeqfzo  14861  cshwcsh2id  14863  wwlktovfo  14993  relexpaddg  15088  iseraltlem2  15715  modfsummods  15825  clim2prod  15920  prodfn0  15926  prodfrec  15927  prodmo  15968  fprodabs  16006  binomfallfac  16073  fprodefsum  16127  dvdsaddre2b  16340  addmodlteqALT  16358  oddge22np1  16382  nn0enne  16410  nn0o1gt2  16414  sumeven  16420  sumodd  16421  dvdslegcd  16537  gcdneg  16555  dfgcd2  16579  rplpwr  16591  lcmf  16666  lcmftp  16669  lcmfunsnlem2lem1  16671  lcmfunsnlem2  16673  lcmfdvdsb  16676  coprmdvds1  16685  qredeq  16690  coprmprod  16694  coprmproddvdslem  16695  cncongr1  16700  cncongr2  16701  prm2orodd  16724  2mulprm  16726  nnnn0modprm0  16839  prm23lt5  16847  prm23ge5  16848  dvdsprmpweqnn  16918  dvdsprmpweqle  16919  oddprmdvds  16936  prmpwdvds  16937  prmreclem4  16952  ramcl  17062  prmgaplem6  17089  prmgaplem7  17090  prmgaplem8  17091  cshwshashlem1  17129  cshwshashlem2  17130  cshwshashlem3  17131  cshwrepswhash1  17136  setsn0fun  17206  setsstruct2  17207  imasleval  17587  mreiincl  17640  mreexexd  17692  inveq  17821  cicsym  17851  cictr  17852  initoid  18054  termoid  18055  initoeu2lem0  18066  initoeu2lem1  18067  initoeu2lem2  18068  initoeu2  18069  fthestrcsetc  18205  fthsetcestrc  18220  drsdirfi  18362  isnmgm  18669  mgmhmlin  18724  issubmgm2  18728  sgrpass  18750  insubm  18843  mgm2nsgrplem3  18945  dfgrp3lem  19068  cyccom  19233  symg2bas  19424  symgfix2  19448  symgextf1  19453  gsmsymgrfix  19460  pmtrprfv3  19486  psgnunilem4  19529  efgi2  19757  0ringnnzr  20541  rnghmsscmap  20646  rnghmsubcsetclem2  20648  rngcinv  20653  funcrngcsetc  20656  funcrngcsetcALT  20657  rhmsscmap  20675  rhmsubcsetclem2  20677  rhmsubcrngclem2  20683  ringcbasbas  20689  funcringcsetc  20690  rhmsubclem4  20704  rngqiprngimfo  21328  psgndiflemB  21635  psgndiflemA  21636  elfrlmbasn0  21800  lmictra  21882  mpfrcl  22126  gsummoncoe1  22327  mamufacex  22415  matecl  22446  dmatelnd  22517  dmatscmcl  22524  scmateALT  22533  scmatsgrp1  22543  scmatf1  22552  mavmulsolcl  22572  cramerimplem1  22704  cramerimplem2  22705  pmatcollpw3fi1  22809  mp2pm2mplem4  22830  pm2mpfo  22835  chmaidscmat  22869  fvmptnn04ifb  22872  chfacfscmul0  22879  chfacfpmmul0  22883  cayhamlem1  22887  cayhamlem3  22908  cayleyhamilton1  22913  fiinopn  22922  tgcl  22991  distop  23017  isclo2  23111  iscldtop  23118  ssnei2  23139  opnnei  23143  pnfnei  23243  mnfnei  23244  tgcnp  23276  cnpnei  23287  1stcelcls  23484  txcnpi  23631  cnmptcom  23701  fbfinnfr  23864  isfildlem  23880  snfil  23887  fbunfip  23892  fgcl  23901  elfm2  23971  fmco  23984  fbflim2  24000  cnpflf2  24023  flimfcls  24049  tmdgsum  24118  neibl  24529  tngngpim  24695  fgcfil  25318  caubl  25355  volsuplem  25603  ellimc3  25928  dvnadd  25979  dvnres  25981  cpnord  25985  dvnfre  26004  ply1divex  26190  cxpmul2  26745  fsumdvdsmul  27252  zabsle1  27354  gausslemma2dlem1a  27423  gausslemma2dlem3  27426  lgsquad2lem2  27443  2lgs  27465  2sq2  27491  2sqnn0  27496  2sqnn  27497  2sqreultlem  27505  2sqreunnltlem  27508  qabvexp  27684  sltval2  27715  nolt02o  27754  ssltun1  27867  scutun12  27869  madebday  27952  mulsprop  28170  precsexlem8  28252  precsexlem9  28253  noseqind  28312  om2noseqrdg  28324  peano5uzs  28404  axcontlem4  28996  umgredgprv  29138  umgrnloop  29139  upgrpredgv  29170  upgredgpr  29173  edglnl  29174  usgredgprvALT  29226  usgrnloopALT  29234  usgredg2v  29258  fusgrfis  29361  nbuhgr2vtx1edgblem  29382  nb3grprlem1  29411  cusgrsize2inds  29485  cusgrfi  29490  fusgrn0degnn0  29531  uspgrloopvtxel  29548  vtxdginducedm1lem4  29574  uhgr0edg0rgrb  29606  wlkl1loop  29670  wlk1walk  29671  upgriswlk  29673  upgrwlkvtxedg  29677  uspgr2wlkeq  29678  wlkv0  29683  wlksoneq1eq2  29696  wlkon2n0  29698  wlkreslem  29701  wlkres  29702  lfgrwlkprop  29719  pthdivtx  29761  2pthnloop  29763  spthonepeq  29784  uhgrwkspthlem2  29786  uhgrwkspth  29787  usgr2wlkneq  29788  usgr2trlncl  29792  usgr2pthlem  29795  usgr2pth  29796  cyclnspth  29832  lfgrn1cycl  29834  usgr2trlncrct  29835  uspgrn2crct  29837  crctcshwlkn0lem3  29841  crctcshwlkn0lem5  29843  wwlknp  29872  wspthneq1eq2  29889  0enwwlksnge1  29893  wlklnwwlkln1  29897  wlkiswwlks2  29904  wlkiswwlksupgr2  29906  wlklnwwlkln2lem  29911  wwlksnred  29921  wwlksnextbi  29923  wwlksnredwwlkn0  29925  wwlksnextwrd  29926  wwlksnextinj  29928  wwlksnextproplem3  29940  wwlksnextprop  29941  wspthsnwspthsnon  29945  wspthsnonn0vne  29946  2pthon3v  29972  umgr2adedgwlkonALT  29976  umgr2wlk  29978  umgr2wlkon  29979  umgrwwlks2on  29986  elwspths2on  29989  usgr2wspthons3  29993  elwwlks2  29995  rusgrnumwwlk  30004  clwwlkccatlem  30017  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwlkclwwlklem2  30028  clwlkclwwlkf1lem3  30034  erclwwlkeqlen  30047  clwwlknwwlksn  30066  loopclwwlkn1b  30070  clwwlkf1  30077  wwlksext2clwwlk  30085  eleclclwwlknlem2  30089  umgr2cwwk2dif  30092  eleclclwwlkn  30104  hashecclwwlkn1  30105  umgrhashecclwwlk  30106  clwwlknonwwlknonb  30134  clwwlknonex2lem2  30136  clwwlknonex2  30137  1pthon2v  30181  upgr3v3e3cycl  30208  uhgr3cyclexlem  30209  uhgr3cyclex  30210  eupth2lem3lem4  30259  frgr3vlem1  30301  frgr3vlem2  30302  3vfriswmgrlem  30305  3vfriswmgr  30306  3cyclfrgrrn1  30313  n4cyclfrgr  30319  frgrncvvdeqlem3  30329  frgrncvvdeqlem6  30332  frgrncvvdeqlem7  30333  frgrncvvdeqlem8  30334  frgrwopreglem4a  30338  frgrwopreglem3  30342  frgrwopreg1  30346  frgrwopreg2  30347  frgrwopreglem5lem  30348  frgrwopreglem5ALT  30350  frgrwopreg  30351  fusgr2wsp2nb  30362  2wspmdisj  30365  numclwwlk1lem2foa  30382  numclwwlk1lem2f1  30385  numclwwlk1lem2fo  30386  numclwwlk1  30389  wlkl0  30395  numclwwlk2lem1  30404  numclwlk2lem2f  30405  numclwlk2lem2f1o  30407  frgrreg  30422  frgrregord013  30423  frgrregord13  30424  friendshipgt3  30426  friendship  30427  eulplig  30513  ipassi  30869  ubthlem2  30899  isch3  31269  shintcli  31357  shmodsi  31417  spansncvi  31680  hoaddsub  31844  eigorthi  31865  pjss2coi  32192  pjnormssi  32196  pj3cor1i  32237  strb  32286  dmdmd  32328  mdsl0  32338  csmdsymi  32362  chrelat2i  32393  mdsymlem3  32433  mdsymlem6  32436  sumdmdlem2  32447  opreu2reuALT  32504  ssrelf  32634  gsumwun  33050  spthcycl  35113  loop1cycl  35121  cvmlift2lem1  35286  satfrel  35351  satfrnmapom  35354  fmlafvel  35369  fmla1  35371  gonarlem  35378  gonar  35379  goalrlem  35380  goalr  35381  satffunlem  35385  satffunlem1lem1  35386  satffunlem2lem1  35388  satffun  35393  satefvfmla1  35409  mrsubvrs  35506  mclsax  35553  3ccased  35698  dfon2lem3  35766  rdgprc  35775  cgrextend  35989  btwndiff  36008  btwnconn1lem12  36079  brsegle  36089  broutsideof2  36103  funray  36121  in-ax8  36206  ss-ax8  36207  elicc3  36299  nn0prpwlem  36304  nn0prpw  36305  fnessref  36339  neibastop2lem  36342  filnetlem4  36363  meran1  36393  waj-ax  36396  arg-ax  36398  bj-nnclavc  36530  bj-con2com  36543  bj-axdd2  36574  bj-alrimg  36601  bj-exlimg  36605  bj-exalimi  36615  bj-cbvalimt  36621  bj-eximcom  36625  bj-ssbid1ALT  36647  bj-sb  36669  bj-snsetex  36945  bj-restpw  37074  bj-finsumval0  37267  mptsnunlem  37320  icoreclin  37339  relowlpssretop  37346  inunissunidif  37357  rdgssun  37360  finorwe  37364  domalom  37386  wl-dral1d  37511  wl-exeq  37514  wl-lem-exsb  37546  poimirlem29  37635  poimirlem32  37638  fdc  37731  seqpo  37733  incsequz  37734  isismty  37787  ismtybndlem  37792  heibor1lem  37795  ismgmOLD  37836  isexid2  37841  ghomco  37877  pridlc  38057  relcnveq3  38302  elrelscnveq3  38472  cdleme18d  40277  tendovalco  40747  cdlemn11pre  41192  dihord2pre  41207  indstrd  42174  unitscyglem3  42178  nnadddir  42283  eu6w  42662  incssnn0  42698  fphpd  42803  jm2.19lem3  42979  setindtr  43012  islssfg2  43059  mpaaeu  43138  ordnexbtwnsuc  43256  oaabsb  43283  succlg  43317  oacl2g  43319  omabs2  43321  omcl2  43322  omcl3g  43323  pr2cv  43537  refimssco  43596  iunrelexpmin1  43697  iunrelexpmin2  43701  trclimalb2  43715  clsk1indlem3  44032  tfindsd  44200  mnurndlem1  44276  nzss  44312  sb5ALT  44522  truniALT  44538  ee223  44631  3orbi123VD  44847  sbc3orgVD  44848  exbirVD  44850  exbiriVD  44851  sbcim2gVD  44872  trsbcVD  44874  truniALTVD  44875  onfrALTlem3VD  44884  onfrALTlem2VD  44886  csbrngVD  44893  19.41rgVD  44899  ax6e2eqVD  44904  ax6e2ndeqVD  44906  2uasbanhVD  44908  sb5ALTVD  44910  vk15.4jVD  44911  infxrunb3rnmpt  45377  stoweidlem26  45981  et-equeucl  46827  hirstL-ax3  46841  rexsb  47048  rexrsb  47049  euoreqb  47058  2reu8i  47062  afvres  47121  tz6.12-afv  47122  afvco2  47125  afv2orxorb  47177  afv2res  47188  tz6.12-afv2  47189  tz6.12i-afv2  47192  dfatcolem  47204  zm1nn  47251  2ffzoeq  47276  smonoord  47295  iccpartiltu  47346  iccpartlt  47348  iccpartltu  47349  iccpartgtl  47350  iccpartgt  47351  iccpartleu  47352  iccpartgel  47353  icceuelpart  47360  iccpartnel  47362  lswn0  47368  ichnreuop  47396  ichreuopeq  47397  prsprel  47411  sprsymrelfvlem  47414  sprsymrelf1lem  47415  sprsymrelfolem2  47417  prproropf1olem4  47430  paireqne  47435  prprelb  47440  reupr  47446  goldbachth  47471  odz2prm2pw  47487  fmtno4prmfac  47496  fmtno4prmfac193  47497  prmdvdsfmtnof1lem2  47509  2pwp1prmfmtno  47514  lighneallem2  47530  lighneallem4b  47533  lighneallem4  47534  requad2  47547  odd2prm2  47642  mogoldbblem  47644  gbepos  47682  gbowgt5  47686  gbowge7  47687  stgoldbwt  47700  sbgoldbwt  47701  sbgoldbst  47702  sbgoldbaltlem1  47703  sbgoldbalt  47705  sbgoldbo  47711  nnsum3primesle9  47718  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  bgoldbtbndlem1  47729  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  bgoldbtbnd  47733  dfnbgr6  47780  isuspgrimlem  47811  uhgrimisgrgric  47836  clnbgrgrim  47839  usgrgrtrirex  47852  isubgr3stgrlem4  47871  grilcbri2  47906  grlicsym  47908  grlictr  47910  gricgrlic  47913  gpgvtxedg0  47955  gpgvtxedg1  47956  upgrwlkupwlk  47983  uspgrsprf1  47990  lmod0rng  48072  lidldomn1  48074  rngccatidALTV  48115  rngcinvALTV  48119  rhmsubcALTVlem4  48127  funcringcsetcALTV2lem9  48141  ringccatidALTV  48149  ringcbasbasALTV  48155  ztprmneprm  48191  pgrpgt2nabl  48210  lmodvsmdi  48223  ply1mulgsumlem2  48232  lincsumcl  48276  ellcoellss  48280  linindslinci  48293  islinindfis  48294  lincext3  48301  lindslinindimp2lem4  48306  lindslinindsimp2lem5  48307  lindslinindsimp2  48308  lindsrng01  48313  ldepspr  48318  lincresunit3lem1  48324  elfzolborelfzop1  48364  dignn0ldlem  48451  nn0sumshdiglem1  48470  1arymaptf1  48491  2arymaptf1  48502  rrx2xpref1o  48567  rrx2plord2  48571  rrx2plordisom  48572  line2ylem  48600  line2xlem  48602  line2y  48604  itschlc0xyqsol1  48615  inlinecirc02plem  48635  fullthinc  48845  tfis2d  48910  onsetrec  48938