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  1349  3expd  1354  mp3an1i  1456  minimp  1621  meredith  1641  19.35  1877  speimfw  1963  equtrr  2022  equeucl  2024  ax12ev2  2181  sbiedw  2317  cbv1v  2338  exsb  2362  cbv1  2407  ax12b  2429  axc11n  2431  dvelimdf  2454  equvel  2461  dfsb1  2486  sbied  2508  dfmoeu  2536  mo3  2564  mo4  2566  2mo  2648  2eu6  2657  exists2  2662  pm2.61dne  3019  rexlimdv  3140  r19.21v  3166  r19.12  3298  2gencl  3508  3gencl  3509  vtocl2ga  3562  vtocl2gaf  3563  vtocl3gaf  3565  vtocl3ga  3567  vtocl4ga  3570  rspccv  3603  ceqex  3636  mob  3705  euind  3712  reuind  3741  2reu1  3877  sseq2  3990  nelss  4029  rexdifi  4130  reupick2  4311  disjeq0  4436  uneqdifeq  4473  sspw  4591  ssprsseq  4806  preq12b  4831  prnebg  4837  prel12g  4845  3elpr2eq  4887  iinss2  5038  trintss  5253  dtruALT2  5345  reusv2lem1  5373  alxfr  5382  ralxfrALT  5390  exexneq  5414  dtruOLD  5421  copsexgw  5470  copsexg  5471  snopeqop  5486  propeqop  5487  opthhausdorff  5497  opthhausdorff0  5498  pofun  5584  solin  5593  frss  5623  2optocl  5755  3optocl  5756  ssrel  5766  ssrelOLD  5767  ssrel2  5769  ssrelrel  5780  relop  5835  dfres3  5976  asymref2  6111  xpidtr  6116  trin2  6117  poltletr  6126  imadifssran  6145  xp11  6169  relcnvtrg  6260  reuop  6287  tz7.7  6383  ordtr2  6402  suc11  6466  iotavalOLD  6510  funmoOLD  6557  fundif  6590  fss  6727  f0dom0  6767  fv3  6899  tz6.12i  6909  mpteqb  7010  fveqdmss  7073  eldmrexrnb  7087  funopsn  7143  funsndifnop  7146  tpres  7198  funfvima  7227  fvclss  7238  f1veqaeq  7254  fvf1pr  7305  isoselem  7339  oprabv  7472  ovg  7577  elovmpt3rab1  7672  sorpsscmpl  7733  iunpw  7770  trom  7875  limom  7882  peano5  7894  focdmex  7959  funelss  8051  funeldmdif  8052  bropopvvv  8094  bropfvvvvlem  8095  f1o2ndf1  8126  poxp  8132  soxp  8133  poxp2  8147  frxp2  8148  frxp3  8155  suppimacnv  8178  ressuppss  8187  ressuppssdif  8189  tposfn2  8252  wfr3g  8326  onnseq  8363  smoel  8379  smogt  8386  smoiso2  8388  tfr3  8418  tz7.48-2  8461  tz7.48-3  8463  tz7.49  8464  oecl  8554  oaordex  8575  oalimcl  8577  oaass  8578  omordi  8583  omlimcl  8595  odi  8596  omeulem1  8599  oen0  8603  nnawordi  8638  nnaass  8639  nnmordi  8648  omabs  8668  omsmolem  8674  naddssim  8702  brinxper  8753  iiner  8808  2ecoptocl  8827  3ecoptocl  8828  undifixp  8953  xpdom2  9086  xpf1o  9158  infensuc  9174  findcard2  9183  php  9226  phpOLD  9236  onomeneqOLD  9243  isinf  9273  isinfOLD  9274  unblem2  9306  fodomfir  9345  infssuni  9363  finsschain  9376  fsuppunfi  9405  fsuppunbi  9406  marypha1  9451  hartogs  9563  card2on  9573  card2inf  9574  xpwdomg  9604  elirrv  9615  en3lp  9633  preleqg  9634  inf3lem1  9647  inf3lem2  9648  inf3lem3  9649  inf3lem5  9651  noinfep  9679  ttrclss  9739  ttrclselem2  9745  trcl  9747  tcel  9764  frr3g  9775  rankonidlem  9847  scottex  9904  djuunxp  9940  eldju2ndl  9943  updjud  9953  dif1card  10029  fodomnum  10076  cardaleph  10108  kmlem9  10178  kmlem13  10182  cflim2  10282  cfsmolem  10289  infpssrlem3  10324  isfin7-2  10415  fin1a2lem6  10424  fin1a2lem12  10430  domtriomlem  10461  axdc3lem4  10472  axdc4lem  10474  zorn2lem3  10517  zorn2lem4  10518  zorn2lem5  10519  zorn2lem7  10521  zornn0g  10524  axdclem2  10539  ondomon  10582  alephval2  10591  cfpwsdom  10603  wuncval2  10766  grupr  10816  gruiun  10818  ingru  10834  grothomex  10848  indpi  10926  nqereu  10948  prlem934  11052  reclem2pr  11067  mulgt0sr  11124  supsrlem  11130  dedekind  11403  lemul1a  12100  squeeze0  12150  peano5nni  12248  nnunb  12502  nn0lt2  12661  nn0le2is012  12662  fzind  12696  nn0ind-raph  12698  zindd  12699  eluzaddOLD  12892  uzin  12897  nn01to3  12962  xnn0xadd0  13268  xmulasslem  13306  icoshft  13495  fzen  13563  uzsubsubfz  13568  elfz0ubfz0  13654  elfz0fzfz0  13655  fz0fzelfz0  13656  elfzmlbp  13661  elfzodifsumelfzo  13752  ssfzo12bi  13782  fzoopth  13783  elfzonelfzo  13790  elfznelfzo  13793  injresinjlem  13808  injresinj  13809  modfzo0difsn  13966  modsumfzodifsn  13967  addmodlteq  13969  ssnn0fi  14008  fsuppmapnn0fiub0  14016  expcllem  14095  expeq0  14115  mulexp  14124  leexp2r  14197  bernneq  14252  facdiv  14310  hasheqf1oi  14374  hashnn0n0nn  14414  hashss  14432  hashgt12el  14445  hashgt12el2  14446  hashimarni  14464  hashle2pr  14500  pr2pwpr  14502  hashge2el2dif  14503  hashge2el2difr  14504  hashtpg  14508  hashge3el3dif  14510  exprelprel  14513  hash1to3  14515  hash3tpde  14516  tpfo  14523  fundmge2nop0  14525  fi1uzind  14530  ccatsymb  14605  swrdnd  14677  swrdnd2  14678  swrdnnn0nd  14679  swrdnd0  14680  pfxnd0  14711  swrdswrdlem  14727  swrdswrd  14728  pfxccatin12lem2a  14750  pfxccatin12lem1  14751  swrdccatin2  14752  pfxccatin12lem2  14754  pfxccatin12lem3  14755  pfxccat3  14757  swrdccat  14758  swrdccat3blem  14762  repsdf2  14801  repswswrd  14807  cshwidxmod  14826  cshwidx0  14829  cshf1  14833  cshweqrep  14844  cshw1  14845  cshwsexaOLD  14848  2cshwcshw  14849  scshwfzeqfzo  14850  cshwcsh2id  14852  wwlktovfo  14982  relexpaddg  15077  iseraltlem2  15704  modfsummods  15814  clim2prod  15909  prodfn0  15915  prodfrec  15916  prodmo  15957  fprodabs  15995  binomfallfac  16062  fprodefsum  16116  dvdsaddre2b  16331  addmodlteqALT  16349  oddge22np1  16373  nn0enne  16401  nn0o1gt2  16405  sumeven  16411  sumodd  16412  dvdslegcd  16528  gcdneg  16546  dfgcd2  16570  rplpwr  16582  lcmf  16657  lcmftp  16660  lcmfunsnlem2lem1  16662  lcmfunsnlem2  16664  lcmfdvdsb  16667  coprmdvds1  16676  qredeq  16681  coprmprod  16685  coprmproddvdslem  16686  cncongr1  16691  cncongr2  16692  prm2orodd  16715  2mulprm  16717  nnnn0modprm0  16831  prm23lt5  16839  prm23ge5  16840  dvdsprmpweqnn  16910  dvdsprmpweqle  16911  oddprmdvds  16928  prmpwdvds  16929  prmreclem4  16944  ramcl  17054  prmgaplem6  17081  prmgaplem7  17082  prmgaplem8  17083  cshwshashlem1  17120  cshwshashlem2  17121  cshwshashlem3  17122  cshwrepswhash1  17127  setsn0fun  17197  setsstruct2  17198  imasleval  17560  mreiincl  17613  mreexexd  17665  inveq  17792  cicsym  17822  cictr  17823  initoid  18019  termoid  18020  initoeu2lem0  18031  initoeu2lem1  18032  initoeu2lem2  18033  initoeu2  18034  fthestrcsetc  18167  fthsetcestrc  18182  drsdirfi  18322  isnmgm  18627  mgmhmlin  18682  issubmgm2  18686  sgrpass  18708  insubm  18801  mgm2nsgrplem3  18903  dfgrp3lem  19026  cyccom  19191  symg2bas  19379  symgfix2  19402  symgextf1  19407  gsmsymgrfix  19414  pmtrprfv3  19440  psgnunilem4  19483  efgi2  19711  0ringnnzr  20490  rnghmsscmap  20595  rnghmsubcsetclem2  20597  rngcinv  20602  funcrngcsetc  20605  funcrngcsetcALT  20606  rhmsscmap  20624  rhmsubcsetclem2  20626  rhmsubcrngclem2  20632  ringcbasbas  20638  funcringcsetc  20639  rhmsubclem4  20653  rngqiprngimfo  21267  psgndiflemB  21565  psgndiflemA  21566  elfrlmbasn0  21728  lmictra  21810  mpfrcl  22048  gsummoncoe1  22251  mamufacex  22339  matecl  22368  dmatelnd  22439  dmatscmcl  22446  scmateALT  22455  scmatsgrp1  22465  scmatf1  22474  mavmulsolcl  22494  cramerimplem1  22626  cramerimplem2  22627  pmatcollpw3fi1  22731  mp2pm2mplem4  22752  pm2mpfo  22757  chmaidscmat  22791  fvmptnn04ifb  22794  chfacfscmul0  22801  chfacfpmmul0  22805  cayhamlem1  22809  cayhamlem3  22830  cayleyhamilton1  22835  fiinopn  22844  tgcl  22912  distop  22938  isclo2  23031  iscldtop  23038  ssnei2  23059  opnnei  23063  pnfnei  23163  mnfnei  23164  tgcnp  23196  cnpnei  23207  1stcelcls  23404  txcnpi  23551  cnmptcom  23621  fbfinnfr  23784  isfildlem  23800  snfil  23807  fbunfip  23812  fgcl  23821  elfm2  23891  fmco  23904  fbflim2  23920  cnpflf2  23943  flimfcls  23969  tmdgsum  24038  neibl  24445  tngngpim  24603  fgcfil  25228  caubl  25265  volsuplem  25513  ellimc3  25837  dvnadd  25888  dvnres  25890  cpnord  25894  dvnfre  25913  ply1divex  26099  cxpmul2  26655  fsumdvdsmul  27162  zabsle1  27264  gausslemma2dlem1a  27333  gausslemma2dlem3  27336  lgsquad2lem2  27353  2lgs  27375  2sq2  27401  2sqnn0  27406  2sqnn  27407  2sqreultlem  27415  2sqreunnltlem  27418  qabvexp  27594  sltval2  27625  nolt02o  27664  ssltun1  27777  scutun12  27779  madebday  27868  mulsprop  28090  precsexlem8  28173  precsexlem9  28174  noseqind  28243  om2noseqrdg  28255  n0cutlt  28306  peano5uzs  28349  expadds  28377  axcontlem4  28951  umgredgprv  29091  umgrnloop  29092  upgrpredgv  29123  upgredgpr  29126  edglnl  29127  usgredgprvALT  29179  usgrnloopALT  29187  usgredg2v  29211  fusgrfis  29314  nbuhgr2vtx1edgblem  29335  nb3grprlem1  29364  cusgrsize2inds  29438  cusgrfi  29443  fusgrn0degnn0  29484  uspgrloopvtxel  29501  vtxdginducedm1lem4  29527  uhgr0edg0rgrb  29559  wlkl1loop  29623  wlk1walk  29624  upgriswlk  29626  upgrwlkvtxedg  29630  uspgr2wlkeq  29631  wlkv0  29636  wlksoneq1eq2  29649  wlkon2n0  29651  wlkreslem  29654  wlkres  29655  lfgrwlkprop  29672  pthdivtx  29714  2pthnloop  29718  spthonepeq  29739  uhgrwkspthlem2  29741  uhgrwkspth  29742  usgr2wlkneq  29743  usgr2trlncl  29747  usgr2pthlem  29750  usgr2pth  29751  cyclnspth  29788  lfgrn1cycl  29792  usgr2trlncrct  29793  uspgrn2crct  29795  crctcshwlkn0lem3  29799  crctcshwlkn0lem5  29801  wwlknp  29830  wspthneq1eq2  29847  0enwwlksnge1  29851  wlklnwwlkln1  29855  wlkiswwlks2  29862  wlkiswwlksupgr2  29864  wlklnwwlkln2lem  29869  wwlksnred  29879  wwlksnextbi  29881  wwlksnredwwlkn0  29883  wwlksnextwrd  29884  wwlksnextinj  29886  wwlksnextproplem3  29898  wwlksnextprop  29899  wspthsnwspthsnon  29903  wspthsnonn0vne  29904  2pthon3v  29930  umgr2adedgwlkonALT  29934  umgr2wlk  29936  umgr2wlkon  29937  umgrwwlks2on  29944  elwspths2on  29947  usgr2wspthons3  29951  elwwlks2  29953  rusgrnumwwlk  29962  clwwlkccatlem  29975  clwlkclwwlklem2a4  29983  clwlkclwwlklem2a  29984  clwlkclwwlklem2  29986  clwlkclwwlkf1lem3  29992  erclwwlkeqlen  30005  clwwlknwwlksn  30024  loopclwwlkn1b  30028  clwwlkf1  30035  wwlksext2clwwlk  30043  eleclclwwlknlem2  30047  umgr2cwwk2dif  30050  eleclclwwlkn  30062  hashecclwwlkn1  30063  umgrhashecclwwlk  30064  clwwlknonwwlknonb  30092  clwwlknonex2lem2  30094  clwwlknonex2  30095  1pthon2v  30139  upgr3v3e3cycl  30166  uhgr3cyclexlem  30167  uhgr3cyclex  30168  eupth2lem3lem4  30217  frgr3vlem1  30259  frgr3vlem2  30260  3vfriswmgrlem  30263  3vfriswmgr  30264  3cyclfrgrrn1  30271  n4cyclfrgr  30277  frgrncvvdeqlem3  30287  frgrncvvdeqlem6  30290  frgrncvvdeqlem7  30291  frgrncvvdeqlem8  30292  frgrwopreglem4a  30296  frgrwopreglem3  30300  frgrwopreg1  30304  frgrwopreg2  30305  frgrwopreglem5lem  30306  frgrwopreglem5ALT  30308  frgrwopreg  30309  fusgr2wsp2nb  30320  2wspmdisj  30323  numclwwlk1lem2foa  30340  numclwwlk1lem2f1  30343  numclwwlk1lem2fo  30344  numclwwlk1  30347  wlkl0  30353  numclwwlk2lem1  30362  numclwlk2lem2f  30363  numclwlk2lem2f1o  30365  frgrreg  30380  frgrregord013  30381  frgrregord13  30382  friendshipgt3  30384  friendship  30385  eulplig  30471  ipassi  30827  ubthlem2  30857  isch3  31227  shintcli  31315  shmodsi  31375  spansncvi  31638  hoaddsub  31802  eigorthi  31823  pjss2coi  32150  pjnormssi  32154  pj3cor1i  32195  strb  32244  dmdmd  32286  mdsl0  32296  csmdsymi  32320  chrelat2i  32351  mdsymlem3  32391  mdsymlem6  32394  sumdmdlem2  32405  opreu2reuALT  32463  ssrelf  32600  gsumwun  33064  spthcycl  35156  loop1cycl  35164  cvmlift2lem1  35329  satfrel  35394  satfrnmapom  35397  fmlafvel  35412  fmla1  35414  gonarlem  35421  gonar  35422  goalrlem  35423  goalr  35424  satffunlem  35428  satffunlem1lem1  35429  satffunlem2lem1  35431  satffun  35436  satefvfmla1  35452  mrsubvrs  35549  mclsax  35596  3ccased  35741  dfon2lem3  35808  rdgprc  35817  cgrextend  36031  btwndiff  36050  btwnconn1lem12  36121  brsegle  36131  broutsideof2  36145  funray  36163  in-ax8  36247  ss-ax8  36248  elicc3  36340  nn0prpwlem  36345  nn0prpw  36346  fnessref  36380  neibastop2lem  36383  filnetlem4  36404  meran1  36434  waj-ax  36437  arg-ax  36439  bj-nnclavc  36571  bj-con2com  36584  bj-axdd2  36615  bj-alrimg  36642  bj-exlimg  36646  bj-exalimi  36656  bj-cbvalimt  36662  bj-eximcom  36666  bj-ssbid1ALT  36688  bj-sb  36710  bj-snsetex  36986  bj-restpw  37115  bj-finsumval0  37308  mptsnunlem  37361  icoreclin  37380  relowlpssretop  37387  inunissunidif  37398  rdgssun  37401  finorwe  37405  domalom  37427  wl-dral1d  37554  wl-exeq  37557  wl-lem-exsb  37589  poimirlem29  37678  poimirlem32  37681  fdc  37774  seqpo  37776  incsequz  37777  isismty  37830  ismtybndlem  37835  heibor1lem  37838  ismgmOLD  37879  isexid2  37884  ghomco  37920  pridlc  38100  relcnveq3  38344  elrelscnveq3  38514  cdleme18d  40319  tendovalco  40789  cdlemn11pre  41234  dihord2pre  41249  indstrd  42211  unitscyglem3  42215  nnadddir  42288  eu6w  42674  incssnn0  42709  fphpd  42814  jm2.19lem3  42990  setindtr  43023  islssfg2  43070  mpaaeu  43149  ordnexbtwnsuc  43266  oaabsb  43293  succlg  43327  oacl2g  43329  omabs2  43331  omcl2  43332  omcl3g  43333  pr2cv  43547  refimssco  43606  iunrelexpmin1  43707  iunrelexpmin2  43711  trclimalb2  43725  clsk1indlem3  44042  tfindsd  44209  mnurndlem1  44280  nzss  44316  sb5ALT  44525  truniALT  44541  ee223  44634  3orbi123VD  44849  sbc3orgVD  44850  exbirVD  44852  exbiriVD  44853  sbcim2gVD  44874  trsbcVD  44876  truniALTVD  44877  onfrALTlem3VD  44886  onfrALTlem2VD  44888  csbrngVD  44895  19.41rgVD  44901  ax6e2eqVD  44906  ax6e2ndeqVD  44908  2uasbanhVD  44910  sb5ALTVD  44912  vk15.4jVD  44913  infxrunb3rnmpt  45435  stoweidlem26  46035  et-equeucl  46881  hirstL-ax3  46901  rexsb  47108  rexrsb  47109  euoreqb  47118  2reu8i  47122  afvres  47181  tz6.12-afv  47182  afvco2  47185  afv2orxorb  47237  afv2res  47248  tz6.12-afv2  47249  tz6.12i-afv2  47252  dfatcolem  47264  zm1nn  47311  2ffzoeq  47336  smonoord  47365  iccpartiltu  47416  iccpartlt  47418  iccpartltu  47419  iccpartgtl  47420  iccpartgt  47421  iccpartleu  47422  iccpartgel  47423  icceuelpart  47430  iccpartnel  47432  lswn0  47438  ichnreuop  47466  ichreuopeq  47467  prsprel  47481  sprsymrelfvlem  47484  sprsymrelf1lem  47485  sprsymrelfolem2  47487  prproropf1olem4  47500  paireqne  47505  prprelb  47510  reupr  47516  goldbachth  47541  odz2prm2pw  47557  fmtno4prmfac  47566  fmtno4prmfac193  47567  prmdvdsfmtnof1lem2  47579  2pwp1prmfmtno  47584  lighneallem2  47600  lighneallem4b  47603  lighneallem4  47604  requad2  47617  odd2prm2  47712  mogoldbblem  47714  gbepos  47752  gbowgt5  47756  gbowge7  47757  stgoldbwt  47770  sbgoldbwt  47771  sbgoldbst  47772  sbgoldbaltlem1  47773  sbgoldbalt  47775  sbgoldbo  47781  nnsum3primesle9  47788  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  bgoldbtbndlem1  47799  bgoldbtbndlem2  47800  bgoldbtbndlem3  47801  bgoldbtbnd  47803  dfnbgr6  47850  isuspgrimlem  47888  uhgrimisgrgric  47924  clnbgrgrim  47927  usgrgrtrirex  47942  isubgr3stgrlem4  47961  grilcbri2  47996  grlicsym  47998  grlictr  48000  gricgrlic  48003  gpgvtxedg0  48047  gpgvtxedg1  48048  upgrwlkupwlk  48095  uspgrsprf1  48102  lmod0rng  48184  lidldomn1  48186  rngccatidALTV  48227  rngcinvALTV  48231  rhmsubcALTVlem4  48239  funcringcsetcALTV2lem9  48253  ringccatidALTV  48261  ringcbasbasALTV  48267  ztprmneprm  48302  pgrpgt2nabl  48321  lmodvsmdi  48334  ply1mulgsumlem2  48343  lincsumcl  48387  ellcoellss  48391  linindslinci  48404  islinindfis  48405  lincext3  48412  lindslinindimp2lem4  48417  lindslinindsimp2lem5  48418  lindslinindsimp2  48419  lindsrng01  48424  ldepspr  48429  lincresunit3lem1  48435  elfzolborelfzop1  48475  dignn0ldlem  48562  nn0sumshdiglem1  48581  1arymaptf1  48602  2arymaptf1  48613  rrx2xpref1o  48678  rrx2plord2  48682  rrx2plordisom  48683  line2ylem  48711  line2xlem  48713  line2y  48715  itschlc0xyqsol1  48726  inlinecirc02plem  48746  fullthinc  49316  tfis2d  49524  onsetrec  49552