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  1622  meredith  1642  19.35  1878  speimfw  1964  equtrr  2023  equeucl  2025  ax12ev2  2185  sbiedw  2319  cbv1v  2338  exsb  2361  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  3015  rexlimdv  3132  r19.21v  3158  r19.12  3282  2gencl  3480  3gencl  3481  vtocl2ga  3530  vtocl2gaf  3531  vtocl3gaf  3533  vtocl3ga  3535  vtocl4ga  3538  rspccv  3570  ceqex  3603  mob  3672  euind  3679  reuind  3708  2reu1  3844  sseq2  3957  nelss  3996  rexdifi  4099  reupick2  4280  disjeq0  4405  uneqdifeq  4442  sspw  4560  ssprsseq  4776  preq12b  4801  prnebg  4807  prel12g  4815  3elpr2eq  4857  iinss2  5008  trintss  5218  dtruALT2  5310  reusv2lem1  5338  alxfr  5347  ralxfrALT  5355  exexneq  5379  copsexgw  5433  copsexg  5434  snopeqop  5449  propeqop  5450  opthhausdorff  5460  opthhausdorff0  5461  pofun  5545  solin  5554  frss  5583  2optocl  5715  3optocl  5716  ssrel  5727  ssrel2  5729  ssrelrel  5740  relop  5794  dfres3  5937  asymref2  6068  xpidtr  6073  trin2  6074  poltletr  6083  imadifssran  6103  xp11  6127  relcnvtrg  6219  reuop  6245  tz7.7  6337  ordtr2  6356  suc11  6420  fundif  6535  fss  6672  f0dom0  6712  fv3  6846  tz6.12i  6854  mpteqb  6954  fveqdmss  7017  eldmrexrnb  7031  funopsn  7087  funsndifnop  7090  tpres  7141  funfvima  7170  fvclss  7181  f1veqaeq  7196  fvf1pr  7247  isoselem  7281  oprabv  7412  ovg  7517  elovmpt3rab1  7612  sorpsscmpl  7673  iunpw  7710  trom  7811  limom  7818  peano5  7829  focdmex  7894  funelss  7985  funeldmdif  7986  bropopvvv  8026  bropfvvvvlem  8027  f1o2ndf1  8058  poxp  8064  soxp  8065  poxp2  8079  frxp2  8080  frxp3  8087  suppimacnv  8110  ressuppss  8119  ressuppssdif  8121  tposfn2  8184  wfr3g  8255  onnseq  8270  smoel  8286  smogt  8293  smoiso2  8295  tfr3  8324  tz7.48-2  8367  tz7.48-3  8369  tz7.49  8370  oecl  8458  oaordex  8479  oalimcl  8481  oaass  8482  omordi  8487  omlimcl  8499  odi  8500  omeulem1  8503  oen0  8507  nnawordi  8542  nnaass  8543  nnmordi  8552  omabs  8572  omsmolem  8578  naddssim  8606  brinxper  8657  iiner  8719  2ecoptocl  8738  3ecoptocl  8739  undifixp  8864  xpdom2  8992  xpf1o  9059  infensuc  9075  findcard2  9081  php  9123  isinf  9156  unblem2  9184  fodomfir  9219  infssuni  9237  finsschain  9250  fsuppunfi  9279  fsuppunbi  9280  marypha1  9325  hartogs  9437  card2on  9447  card2inf  9448  xpwdomg  9478  elirrv  9490  elirrvOLD  9491  en3lp  9511  preleqg  9512  inf3lem1  9525  inf3lem2  9526  inf3lem3  9527  inf3lem5  9529  noinfep  9557  ttrclss  9617  ttrclselem2  9623  trcl  9625  tcel  9640  frr3g  9656  rankonidlem  9728  scottex  9785  djuunxp  9821  eldju2ndl  9824  updjud  9834  dif1card  9908  fodomnum  9955  cardaleph  9987  kmlem9  10057  kmlem13  10061  cflim2  10161  cfsmolem  10168  infpssrlem3  10203  isfin7-2  10294  fin1a2lem6  10303  fin1a2lem12  10309  domtriomlem  10340  axdc3lem4  10351  axdc4lem  10353  zorn2lem3  10396  zorn2lem4  10397  zorn2lem5  10398  zorn2lem7  10400  zornn0g  10403  axdclem2  10418  ondomon  10461  alephval2  10470  cfpwsdom  10482  wuncval2  10645  grupr  10695  gruiun  10697  ingru  10713  grothomex  10727  indpi  10805  nqereu  10827  prlem934  10931  reclem2pr  10946  mulgt0sr  11003  supsrlem  11009  1re  11119  dedekind  11283  lemul1a  11982  squeeze0  12032  peano5nni  12135  nnunb  12384  nn0lt2  12542  nn0le2is012  12543  fzind  12577  nn0ind-raph  12579  zindd  12580  uzin  12774  nn01to3  12841  xnn0xadd0  13148  xmulasslem  13186  icoshft  13375  fzen  13443  uzsubsubfz  13448  elfz0ubfz0  13534  elfz0fzfz0  13535  fz0fzelfz0  13536  elfzmlbp  13541  elfzodifsumelfzo  13633  ssfzo12bi  13663  fzoopth  13664  elfzonelfzo  13671  elfznelfzo  13675  injresinjlem  13692  injresinj  13693  modfzo0difsn  13852  modsumfzodifsn  13853  addmodlteq  13855  ssnn0fi  13894  fsuppmapnn0fiub0  13902  expcllem  13981  expeq0  14001  mulexp  14010  leexp2r  14083  bernneq  14138  facdiv  14196  hasheqf1oi  14260  hashnn0n0nn  14300  hashss  14318  hashgt12el  14331  hashgt12el2  14332  hashimarni  14350  hashle2pr  14386  pr2pwpr  14388  hashge2el2dif  14389  hashge2el2difr  14390  hashtpg  14394  hashge3el3dif  14396  exprelprel  14399  hash1to3  14401  hash3tpde  14402  tpfo  14409  fundmge2nop0  14411  fi1uzind  14416  ccatsymb  14492  swrdnd  14564  swrdnd2  14565  swrdnnn0nd  14566  swrdnd0  14567  pfxnd0  14598  swrdswrdlem  14613  swrdswrd  14614  pfxccatin12lem2a  14636  pfxccatin12lem1  14637  swrdccatin2  14638  pfxccatin12lem2  14640  pfxccatin12lem3  14641  pfxccat3  14643  swrdccat  14644  swrdccat3blem  14648  repsdf2  14687  repswswrd  14693  cshwidxmod  14712  cshwidx0  14715  cshf1  14719  cshweqrep  14730  cshw1  14731  2cshwcshw  14734  scshwfzeqfzo  14735  cshwcsh2id  14737  wwlktovfo  14867  relexpaddg  14962  iseraltlem2  15592  modfsummods  15702  clim2prod  15797  prodfn0  15803  prodfrec  15804  prodmo  15845  fprodabs  15883  binomfallfac  15950  fprodefsum  16004  dvdsaddre2b  16220  addmodlteqALT  16238  oddge22np1  16262  nn0enne  16290  nn0o1gt2  16294  sumeven  16300  sumodd  16301  dvdslegcd  16417  gcdneg  16435  dfgcd2  16459  rplpwr  16471  lcmf  16546  lcmftp  16549  lcmfunsnlem2lem1  16551  lcmfunsnlem2  16553  lcmfdvdsb  16556  coprmdvds1  16565  qredeq  16570  coprmprod  16574  coprmproddvdslem  16575  cncongr1  16580  cncongr2  16581  prm2orodd  16604  2mulprm  16606  nnnn0modprm0  16720  prm23lt5  16728  prm23ge5  16729  dvdsprmpweqnn  16799  dvdsprmpweqle  16800  oddprmdvds  16817  prmpwdvds  16818  prmreclem4  16833  ramcl  16943  prmgaplem6  16970  prmgaplem7  16971  prmgaplem8  16972  cshwshashlem1  17009  cshwshashlem2  17010  cshwshashlem3  17011  cshwrepswhash1  17016  setsn0fun  17086  setsstruct2  17087  imasleval  17447  mreiincl  17500  mreexexd  17556  inveq  17683  cicsym  17713  cictr  17714  initoid  17910  termoid  17911  initoeu2lem0  17922  initoeu2lem1  17923  initoeu2lem2  17924  initoeu2  17925  fthestrcsetc  18058  fthsetcestrc  18073  drsdirfi  18213  isnmgm  18554  mgmhmlin  18609  issubmgm2  18613  sgrpass  18635  insubm  18728  mgm2nsgrplem3  18830  dfgrp3lem  18953  cyccom  19117  symg2bas  19307  symgfix2  19330  symgextf1  19335  gsmsymgrfix  19342  pmtrprfv3  19368  psgnunilem4  19411  efgi2  19639  0ringnnzr  20442  rnghmsscmap  20547  rnghmsubcsetclem2  20549  rngcinv  20554  funcrngcsetc  20557  funcrngcsetcALT  20558  rhmsscmap  20576  rhmsubcsetclem2  20578  rhmsubcrngclem2  20584  ringcbasbas  20590  funcringcsetc  20591  rhmsubclem4  20605  rngqiprngimfo  21240  psgndiflemB  21539  psgndiflemA  21540  elfrlmbasn0  21702  lmictra  21784  mpfrcl  22021  gsummoncoe1  22224  mamufacex  22312  matecl  22341  dmatelnd  22412  dmatscmcl  22419  scmateALT  22428  scmatsgrp1  22438  scmatf1  22447  mavmulsolcl  22467  cramerimplem1  22599  cramerimplem2  22600  pmatcollpw3fi1  22704  mp2pm2mplem4  22725  pm2mpfo  22730  chmaidscmat  22764  fvmptnn04ifb  22767  chfacfscmul0  22774  chfacfpmmul0  22778  cayhamlem1  22782  cayhamlem3  22803  cayleyhamilton1  22808  fiinopn  22817  tgcl  22885  distop  22911  isclo2  23004  iscldtop  23011  ssnei2  23032  opnnei  23036  pnfnei  23136  mnfnei  23137  tgcnp  23169  cnpnei  23180  1stcelcls  23377  txcnpi  23524  cnmptcom  23594  fbfinnfr  23757  isfildlem  23773  snfil  23780  fbunfip  23785  fgcl  23794  elfm2  23864  fmco  23877  fbflim2  23893  cnpflf2  23916  flimfcls  23942  tmdgsum  24011  neibl  24417  tngngpim  24575  fgcfil  25199  caubl  25236  volsuplem  25484  ellimc3  25808  dvnadd  25859  dvnres  25861  cpnord  25865  dvnfre  25884  ply1divex  26070  cxpmul2  26626  fsumdvdsmul  27133  zabsle1  27235  gausslemma2dlem1a  27304  gausslemma2dlem3  27307  lgsquad2lem2  27324  2lgs  27346  2sq2  27372  2sqnn0  27377  2sqnn  27378  2sqreultlem  27386  2sqreunnltlem  27389  qabvexp  27565  sltval2  27596  nolt02o  27635  ssltun1  27750  scutun12  27752  madebday  27846  mulsprop  28070  precsexlem8  28153  precsexlem9  28154  noseqind  28223  om2noseqrdg  28235  n0cutlt  28286  peano5uzs  28329  expadds  28359  axcontlem4  28947  umgredgprv  29087  umgrnloop  29088  upgrpredgv  29119  upgredgpr  29122  edglnl  29123  usgredgprvALT  29175  usgrnloopALT  29183  usgredg2v  29207  fusgrfis  29310  nbuhgr2vtx1edgblem  29331  nb3grprlem1  29360  cusgrsize2inds  29434  cusgrfi  29439  fusgrn0degnn0  29480  uspgrloopvtxel  29497  vtxdginducedm1lem4  29523  uhgr0edg0rgrb  29555  wlkl1loop  29618  wlk1walk  29619  upgriswlk  29621  upgrwlkvtxedg  29625  uspgr2wlkeq  29626  wlkv0  29630  wlksoneq1eq2  29643  wlkon2n0  29645  wlkreslem  29648  wlkres  29649  lfgrwlkprop  29666  pthdivtx  29707  2pthnloop  29711  spthonepeq  29732  uhgrwkspthlem2  29734  uhgrwkspth  29735  usgr2wlkneq  29736  usgr2trlncl  29740  usgr2pthlem  29743  usgr2pth  29744  cyclnspth  29781  lfgrn1cycl  29785  usgr2trlncrct  29786  uspgrn2crct  29788  crctcshwlkn0lem3  29792  crctcshwlkn0lem5  29794  wwlknp  29823  wspthneq1eq2  29840  0enwwlksnge1  29844  wlklnwwlkln1  29848  wlkiswwlks2  29855  wlkiswwlksupgr2  29857  wlklnwwlkln2lem  29862  wwlksnred  29872  wwlksnextbi  29874  wwlksnredwwlkn0  29876  wwlksnextwrd  29877  wwlksnextinj  29879  wwlksnextproplem3  29891  wwlksnextprop  29892  wspthsnwspthsnon  29896  wspthsnonn0vne  29897  2pthon3v  29923  umgr2adedgwlkonALT  29927  umgr2wlk  29929  umgr2wlkon  29930  usgrwwlks2on  29938  umgrwwlks2on  29939  elwspths2on  29942  elwspths2onw  29943  usgr2wspthons3  29947  elwwlks2  29949  rusgrnumwwlk  29958  clwwlkccatlem  29971  clwlkclwwlklem2a4  29979  clwlkclwwlklem2a  29980  clwlkclwwlklem2  29982  clwlkclwwlkf1lem3  29988  erclwwlkeqlen  30001  clwwlknwwlksn  30020  loopclwwlkn1b  30024  clwwlkf1  30031  wwlksext2clwwlk  30039  eleclclwwlknlem2  30043  umgr2cwwk2dif  30046  eleclclwwlkn  30058  hashecclwwlkn1  30059  umgrhashecclwwlk  30060  clwwlknonwwlknonb  30088  clwwlknonex2lem2  30090  clwwlknonex2  30091  1pthon2v  30135  upgr3v3e3cycl  30162  uhgr3cyclexlem  30163  uhgr3cyclex  30164  eupth2lem3lem4  30213  frgr3vlem1  30255  frgr3vlem2  30256  3vfriswmgrlem  30259  3vfriswmgr  30260  3cyclfrgrrn1  30267  n4cyclfrgr  30273  frgrncvvdeqlem3  30283  frgrncvvdeqlem6  30286  frgrncvvdeqlem7  30287  frgrncvvdeqlem8  30288  frgrwopreglem4a  30292  frgrwopreglem3  30296  frgrwopreg1  30300  frgrwopreg2  30301  frgrwopreglem5lem  30302  frgrwopreglem5ALT  30304  frgrwopreg  30305  fusgr2wsp2nb  30316  2wspmdisj  30319  numclwwlk1lem2foa  30336  numclwwlk1lem2f1  30339  numclwwlk1lem2fo  30340  numclwwlk1  30343  wlkl0  30349  numclwwlk2lem1  30358  numclwlk2lem2f  30359  numclwlk2lem2f1o  30361  frgrreg  30376  frgrregord013  30377  frgrregord13  30378  friendshipgt3  30380  friendship  30381  eulplig  30467  ipassi  30823  ubthlem2  30853  isch3  31223  shintcli  31311  shmodsi  31371  spansncvi  31634  hoaddsub  31798  eigorthi  31819  pjss2coi  32146  pjnormssi  32150  pj3cor1i  32191  strb  32240  dmdmd  32282  mdsl0  32292  csmdsymi  32316  chrelat2i  32347  mdsymlem3  32387  mdsymlem6  32390  sumdmdlem2  32401  opreu2reuALT  32458  ssrelf  32600  gsumwun  33052  r1filim  35136  trssfir1om  35143  trssfir1omregs  35153  onvf1odlem4  35171  spthcycl  35194  loop1cycl  35202  cvmlift2lem1  35367  satfrel  35432  satfrnmapom  35435  fmlafvel  35450  fmla1  35452  gonarlem  35459  gonar  35460  goalrlem  35461  goalr  35462  satffunlem  35466  satffunlem1lem1  35467  satffunlem2lem1  35469  satffun  35474  satefvfmla1  35490  mrsubvrs  35587  mclsax  35634  3ccased  35784  dfon2lem3  35848  rdgprc  35857  cgrextend  36073  btwndiff  36092  btwnconn1lem12  36163  brsegle  36173  broutsideof2  36187  funray  36205  in-ax8  36289  ss-ax8  36290  elicc3  36382  nn0prpwlem  36387  nn0prpw  36388  fnessref  36422  neibastop2lem  36425  filnetlem4  36446  meran1  36476  waj-ax  36479  arg-ax  36481  bj-nnclavc  36613  bj-con2com  36626  bj-axdd2  36657  bj-alrimg  36684  bj-exlimg  36688  bj-exalimi  36698  bj-cbvalimt  36704  bj-eximcom  36708  bj-ssbid1ALT  36730  bj-sb  36752  bj-snsetex  37028  bj-restpw  37157  bj-finsumval0  37350  mptsnunlem  37403  icoreclin  37422  relowlpssretop  37429  inunissunidif  37440  rdgssun  37443  finorwe  37447  domalom  37469  wl-dral1d  37596  wl-exeq  37599  wl-lem-exsb  37631  poimirlem29  37709  poimirlem32  37712  fdc  37805  seqpo  37807  incsequz  37808  isismty  37861  ismtybndlem  37866  heibor1lem  37869  ismgmOLD  37910  isexid2  37915  ghomco  37951  pridlc  38131  relcnveq3  38379  elrelscnveq3  38659  cdleme18d  40414  tendovalco  40884  cdlemn11pre  41329  dihord2pre  41344  indstrd  42306  unitscyglem3  42310  nnadddir  42388  eu6w  42794  incssnn0  42828  fphpd  42933  jm2.19lem3  43108  setindtr  43141  islssfg2  43188  mpaaeu  43267  ordnexbtwnsuc  43384  oaabsb  43411  succlg  43445  oacl2g  43447  omabs2  43449  omcl2  43450  omcl3g  43451  pr2cv  43665  refimssco  43724  iunrelexpmin1  43825  iunrelexpmin2  43829  trclimalb2  43843  clsk1indlem3  44160  tfindsd  44327  mnurndlem1  44398  nzss  44434  sb5ALT  44642  truniALT  44658  ee223  44751  3orbi123VD  44966  sbc3orgVD  44967  exbirVD  44969  exbiriVD  44970  sbcim2gVD  44991  trsbcVD  44993  truniALTVD  44994  onfrALTlem3VD  45003  onfrALTlem2VD  45005  csbrngVD  45012  19.41rgVD  45018  ax6e2eqVD  45023  ax6e2ndeqVD  45025  2uasbanhVD  45027  sb5ALTVD  45029  vk15.4jVD  45030  infxrunb3rnmpt  45550  stoweidlem26  46148  et-equeucl  46994  hirstL-ax3  47016  rexsb  47223  rexrsb  47224  euoreqb  47233  2reu8i  47237  afvres  47296  tz6.12-afv  47297  afvco2  47300  afv2orxorb  47352  afv2res  47363  tz6.12-afv2  47364  tz6.12i-afv2  47367  dfatcolem  47379  zm1nn  47426  2ffzoeq  47451  smonoord  47495  iccpartiltu  47546  iccpartlt  47548  iccpartltu  47549  iccpartgtl  47550  iccpartgt  47551  iccpartleu  47552  iccpartgel  47553  icceuelpart  47560  iccpartnel  47562  lswn0  47568  ichnreuop  47596  ichreuopeq  47597  prsprel  47611  sprsymrelfvlem  47614  sprsymrelf1lem  47615  sprsymrelfolem2  47617  prproropf1olem4  47630  paireqne  47635  prprelb  47640  reupr  47646  goldbachth  47671  odz2prm2pw  47687  fmtno4prmfac  47696  fmtno4prmfac193  47697  prmdvdsfmtnof1lem2  47709  2pwp1prmfmtno  47714  lighneallem2  47730  lighneallem4b  47733  lighneallem4  47734  requad2  47747  odd2prm2  47842  mogoldbblem  47844  gbepos  47882  gbowgt5  47886  gbowge7  47887  stgoldbwt  47900  sbgoldbwt  47901  sbgoldbst  47902  sbgoldbaltlem1  47903  sbgoldbalt  47905  sbgoldbo  47911  nnsum3primesle9  47918  nnsum4primesodd  47920  nnsum4primesoddALTV  47921  nnsum4primeseven  47924  nnsum4primesevenALTV  47925  bgoldbtbndlem1  47929  bgoldbtbndlem2  47930  bgoldbtbndlem3  47931  bgoldbtbnd  47933  dfnbgr6  47981  isuspgrimlem  48019  uhgrimisgrgric  48055  clnbgrgrim  48058  usgrgrtrirex  48074  isubgr3stgrlem4  48093  grilcbri2  48135  grlicsym  48137  grlictr  48139  gricgrlic  48142  gpgvtxedg0  48187  gpgvtxedg1  48188  gpgedg2ov  48190  gpgedg2iv  48191  pgnioedg1  48232  pgnioedg2  48233  pgnioedg3  48234  pgnioedg4  48235  pgnioedg5  48236  pgnbgreunbgrlem2lem3  48240  pgnbgreunbgrlem3  48242  pgnbgreunbgrlem5lem1  48244  pgnbgreunbgrlem5lem2  48245  pgnbgreunbgrlem5lem3  48246  pgnbgreunbgrlem6  48248  upgrwlkupwlk  48264  uspgrsprf1  48271  lmod0rng  48353  lidldomn1  48355  rngccatidALTV  48396  rngcinvALTV  48400  rhmsubcALTVlem4  48408  funcringcsetcALTV2lem9  48422  ringccatidALTV  48430  ringcbasbasALTV  48436  ztprmneprm  48471  pgrpgt2nabl  48490  lmodvsmdi  48503  ply1mulgsumlem2  48512  lincsumcl  48556  ellcoellss  48560  linindslinci  48573  islinindfis  48574  lincext3  48581  lindslinindimp2lem4  48586  lindslinindsimp2lem5  48587  lindslinindsimp2  48588  lindsrng01  48593  ldepspr  48598  lincresunit3lem1  48604  elfzolborelfzop1  48644  dignn0ldlem  48727  nn0sumshdiglem1  48746  1arymaptf1  48767  2arymaptf1  48778  rrx2xpref1o  48843  rrx2plord2  48847  rrx2plordisom  48848  line2ylem  48876  line2xlem  48878  line2y  48880  itschlc0xyqsol1  48891  inlinecirc02plem  48911  fullthinc  49575  tfis2d  49805  onsetrec  49833