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  2183  sbiedw  2317  cbv1v  2336  exsb  2359  cbv1  2402  ax12b  2424  axc11n  2426  dvelimdf  2449  equvel  2456  dfsb1  2481  sbied  2503  dfmoeu  2531  mo3  2559  mo4  2561  2mo  2643  2eu6  2652  exists2  2657  pm2.61dne  3014  rexlimdv  3131  r19.21v  3157  r19.12  3281  2gencl  3479  3gencl  3480  vtocl2ga  3533  vtocl2gaf  3534  vtocl3gaf  3536  vtocl3ga  3538  vtocl4ga  3541  rspccv  3574  ceqex  3607  mob  3676  euind  3683  reuind  3712  2reu1  3848  sseq2  3961  nelss  4000  rexdifi  4100  reupick2  4281  disjeq0  4406  uneqdifeq  4443  sspw  4561  ssprsseq  4777  preq12b  4802  prnebg  4808  prel12g  4816  3elpr2eq  4858  iinss2  5006  trintss  5216  dtruALT2  5308  reusv2lem1  5336  alxfr  5345  ralxfrALT  5353  exexneq  5377  copsexgw  5430  copsexg  5431  snopeqop  5446  propeqop  5447  opthhausdorff  5457  opthhausdorff0  5458  pofun  5542  solin  5551  frss  5580  2optocl  5712  3optocl  5713  ssrel  5723  ssrel2  5725  ssrelrel  5736  relop  5790  dfres3  5933  asymref2  6064  xpidtr  6069  trin2  6070  poltletr  6079  imadifssran  6098  xp11  6122  relcnvtrg  6214  reuop  6240  tz7.7  6332  ordtr2  6351  suc11  6415  fundif  6530  fss  6667  f0dom0  6707  fv3  6840  tz6.12i  6848  mpteqb  6948  fveqdmss  7011  eldmrexrnb  7025  funopsn  7081  funsndifnop  7084  tpres  7135  funfvima  7164  fvclss  7175  f1veqaeq  7190  fvf1pr  7241  isoselem  7275  oprabv  7406  ovg  7511  elovmpt3rab1  7606  sorpsscmpl  7667  iunpw  7704  trom  7805  limom  7812  peano5  7823  focdmex  7888  funelss  7979  funeldmdif  7980  bropopvvv  8020  bropfvvvvlem  8021  f1o2ndf1  8052  poxp  8058  soxp  8059  poxp2  8073  frxp2  8074  frxp3  8081  suppimacnv  8104  ressuppss  8113  ressuppssdif  8115  tposfn2  8178  wfr3g  8249  onnseq  8264  smoel  8280  smogt  8287  smoiso2  8289  tfr3  8318  tz7.48-2  8361  tz7.48-3  8363  tz7.49  8364  oecl  8452  oaordex  8473  oalimcl  8475  oaass  8476  omordi  8481  omlimcl  8493  odi  8494  omeulem1  8497  oen0  8501  nnawordi  8536  nnaass  8537  nnmordi  8546  omabs  8566  omsmolem  8572  naddssim  8600  brinxper  8651  iiner  8713  2ecoptocl  8732  3ecoptocl  8733  undifixp  8858  xpdom2  8985  xpf1o  9052  infensuc  9068  findcard2  9074  php  9116  isinf  9149  unblem2  9177  fodomfir  9212  infssuni  9230  finsschain  9243  fsuppunfi  9272  fsuppunbi  9273  marypha1  9318  hartogs  9430  card2on  9440  card2inf  9441  xpwdomg  9471  elirrv  9483  elirrvOLD  9484  en3lp  9504  preleqg  9505  inf3lem1  9518  inf3lem2  9519  inf3lem3  9520  inf3lem5  9522  noinfep  9550  ttrclss  9610  ttrclselem2  9616  trcl  9618  tcel  9635  frr3g  9646  rankonidlem  9718  scottex  9775  djuunxp  9811  eldju2ndl  9814  updjud  9824  dif1card  9898  fodomnum  9945  cardaleph  9977  kmlem9  10047  kmlem13  10051  cflim2  10151  cfsmolem  10158  infpssrlem3  10193  isfin7-2  10284  fin1a2lem6  10293  fin1a2lem12  10299  domtriomlem  10330  axdc3lem4  10341  axdc4lem  10343  zorn2lem3  10386  zorn2lem4  10387  zorn2lem5  10388  zorn2lem7  10390  zornn0g  10393  axdclem2  10408  ondomon  10451  alephval2  10460  cfpwsdom  10472  wuncval2  10635  grupr  10685  gruiun  10687  ingru  10703  grothomex  10717  indpi  10795  nqereu  10817  prlem934  10921  reclem2pr  10936  mulgt0sr  10993  supsrlem  10999  1re  11109  dedekind  11273  lemul1a  11972  squeeze0  12022  peano5nni  12125  nnunb  12374  nn0lt2  12533  nn0le2is012  12534  fzind  12568  nn0ind-raph  12570  zindd  12571  eluzaddOLD  12764  uzin  12769  nn01to3  12836  xnn0xadd0  13143  xmulasslem  13181  icoshft  13370  fzen  13438  uzsubsubfz  13443  elfz0ubfz0  13529  elfz0fzfz0  13530  fz0fzelfz0  13531  elfzmlbp  13536  elfzodifsumelfzo  13628  ssfzo12bi  13658  fzoopth  13659  elfzonelfzo  13666  elfznelfzo  13670  injresinjlem  13687  injresinj  13688  modfzo0difsn  13847  modsumfzodifsn  13848  addmodlteq  13850  ssnn0fi  13889  fsuppmapnn0fiub0  13897  expcllem  13976  expeq0  13996  mulexp  14005  leexp2r  14078  bernneq  14133  facdiv  14191  hasheqf1oi  14255  hashnn0n0nn  14295  hashss  14313  hashgt12el  14326  hashgt12el2  14327  hashimarni  14345  hashle2pr  14381  pr2pwpr  14383  hashge2el2dif  14384  hashge2el2difr  14385  hashtpg  14389  hashge3el3dif  14391  exprelprel  14394  hash1to3  14396  hash3tpde  14397  tpfo  14404  fundmge2nop0  14406  fi1uzind  14411  ccatsymb  14487  swrdnd  14559  swrdnd2  14560  swrdnnn0nd  14561  swrdnd0  14562  pfxnd0  14593  swrdswrdlem  14608  swrdswrd  14609  pfxccatin12lem2a  14631  pfxccatin12lem1  14632  swrdccatin2  14633  pfxccatin12lem2  14635  pfxccatin12lem3  14636  pfxccat3  14638  swrdccat  14639  swrdccat3blem  14643  repsdf2  14682  repswswrd  14688  cshwidxmod  14707  cshwidx0  14710  cshf1  14714  cshweqrep  14725  cshw1  14726  2cshwcshw  14729  scshwfzeqfzo  14730  cshwcsh2id  14732  wwlktovfo  14862  relexpaddg  14957  iseraltlem2  15587  modfsummods  15697  clim2prod  15792  prodfn0  15798  prodfrec  15799  prodmo  15840  fprodabs  15878  binomfallfac  15945  fprodefsum  15999  dvdsaddre2b  16215  addmodlteqALT  16233  oddge22np1  16257  nn0enne  16285  nn0o1gt2  16289  sumeven  16295  sumodd  16296  dvdslegcd  16412  gcdneg  16430  dfgcd2  16454  rplpwr  16466  lcmf  16541  lcmftp  16544  lcmfunsnlem2lem1  16546  lcmfunsnlem2  16548  lcmfdvdsb  16551  coprmdvds1  16560  qredeq  16565  coprmprod  16569  coprmproddvdslem  16570  cncongr1  16575  cncongr2  16576  prm2orodd  16599  2mulprm  16601  nnnn0modprm0  16715  prm23lt5  16723  prm23ge5  16724  dvdsprmpweqnn  16794  dvdsprmpweqle  16795  oddprmdvds  16812  prmpwdvds  16813  prmreclem4  16828  ramcl  16938  prmgaplem6  16965  prmgaplem7  16966  prmgaplem8  16967  cshwshashlem1  17004  cshwshashlem2  17005  cshwshashlem3  17006  cshwrepswhash1  17011  setsn0fun  17081  setsstruct2  17082  imasleval  17442  mreiincl  17495  mreexexd  17551  inveq  17678  cicsym  17708  cictr  17709  initoid  17905  termoid  17906  initoeu2lem0  17917  initoeu2lem1  17918  initoeu2lem2  17919  initoeu2  17920  fthestrcsetc  18053  fthsetcestrc  18068  drsdirfi  18208  isnmgm  18549  mgmhmlin  18604  issubmgm2  18608  sgrpass  18630  insubm  18723  mgm2nsgrplem3  18825  dfgrp3lem  18948  cyccom  19113  symg2bas  19303  symgfix2  19326  symgextf1  19331  gsmsymgrfix  19338  pmtrprfv3  19364  psgnunilem4  19407  efgi2  19635  0ringnnzr  20438  rnghmsscmap  20543  rnghmsubcsetclem2  20545  rngcinv  20550  funcrngcsetc  20553  funcrngcsetcALT  20554  rhmsscmap  20572  rhmsubcsetclem2  20574  rhmsubcrngclem2  20580  ringcbasbas  20586  funcringcsetc  20587  rhmsubclem4  20601  rngqiprngimfo  21236  psgndiflemB  21535  psgndiflemA  21536  elfrlmbasn0  21698  lmictra  21780  mpfrcl  22018  gsummoncoe1  22221  mamufacex  22309  matecl  22338  dmatelnd  22409  dmatscmcl  22416  scmateALT  22425  scmatsgrp1  22435  scmatf1  22444  mavmulsolcl  22464  cramerimplem1  22596  cramerimplem2  22597  pmatcollpw3fi1  22701  mp2pm2mplem4  22722  pm2mpfo  22727  chmaidscmat  22761  fvmptnn04ifb  22764  chfacfscmul0  22771  chfacfpmmul0  22775  cayhamlem1  22779  cayhamlem3  22800  cayleyhamilton1  22805  fiinopn  22814  tgcl  22882  distop  22908  isclo2  23001  iscldtop  23008  ssnei2  23029  opnnei  23033  pnfnei  23133  mnfnei  23134  tgcnp  23166  cnpnei  23177  1stcelcls  23374  txcnpi  23521  cnmptcom  23591  fbfinnfr  23754  isfildlem  23770  snfil  23777  fbunfip  23782  fgcl  23791  elfm2  23861  fmco  23874  fbflim2  23890  cnpflf2  23913  flimfcls  23939  tmdgsum  24008  neibl  24414  tngngpim  24572  fgcfil  25196  caubl  25233  volsuplem  25481  ellimc3  25805  dvnadd  25856  dvnres  25858  cpnord  25862  dvnfre  25881  ply1divex  26067  cxpmul2  26623  fsumdvdsmul  27130  zabsle1  27232  gausslemma2dlem1a  27301  gausslemma2dlem3  27304  lgsquad2lem2  27321  2lgs  27343  2sq2  27369  2sqnn0  27374  2sqnn  27375  2sqreultlem  27383  2sqreunnltlem  27386  qabvexp  27562  sltval2  27593  nolt02o  27632  ssltun1  27747  scutun12  27749  madebday  27843  mulsprop  28067  precsexlem8  28150  precsexlem9  28151  noseqind  28220  om2noseqrdg  28232  n0cutlt  28283  peano5uzs  28326  expadds  28356  axcontlem4  28943  umgredgprv  29083  umgrnloop  29084  upgrpredgv  29115  upgredgpr  29118  edglnl  29119  usgredgprvALT  29171  usgrnloopALT  29179  usgredg2v  29203  fusgrfis  29306  nbuhgr2vtx1edgblem  29327  nb3grprlem1  29356  cusgrsize2inds  29430  cusgrfi  29435  fusgrn0degnn0  29476  uspgrloopvtxel  29493  vtxdginducedm1lem4  29519  uhgr0edg0rgrb  29551  wlkl1loop  29614  wlk1walk  29615  upgriswlk  29617  upgrwlkvtxedg  29621  uspgr2wlkeq  29622  wlkv0  29626  wlksoneq1eq2  29639  wlkon2n0  29641  wlkreslem  29644  wlkres  29645  lfgrwlkprop  29662  pthdivtx  29703  2pthnloop  29707  spthonepeq  29728  uhgrwkspthlem2  29730  uhgrwkspth  29731  usgr2wlkneq  29732  usgr2trlncl  29736  usgr2pthlem  29739  usgr2pth  29740  cyclnspth  29777  lfgrn1cycl  29781  usgr2trlncrct  29782  uspgrn2crct  29784  crctcshwlkn0lem3  29788  crctcshwlkn0lem5  29790  wwlknp  29819  wspthneq1eq2  29836  0enwwlksnge1  29840  wlklnwwlkln1  29844  wlkiswwlks2  29851  wlkiswwlksupgr2  29853  wlklnwwlkln2lem  29858  wwlksnred  29868  wwlksnextbi  29870  wwlksnredwwlkn0  29872  wwlksnextwrd  29873  wwlksnextinj  29875  wwlksnextproplem3  29887  wwlksnextprop  29888  wspthsnwspthsnon  29892  wspthsnonn0vne  29893  2pthon3v  29919  umgr2adedgwlkonALT  29923  umgr2wlk  29925  umgr2wlkon  29926  umgrwwlks2on  29933  elwspths2on  29936  usgr2wspthons3  29940  elwwlks2  29942  rusgrnumwwlk  29951  clwwlkccatlem  29964  clwlkclwwlklem2a4  29972  clwlkclwwlklem2a  29973  clwlkclwwlklem2  29975  clwlkclwwlkf1lem3  29981  erclwwlkeqlen  29994  clwwlknwwlksn  30013  loopclwwlkn1b  30017  clwwlkf1  30024  wwlksext2clwwlk  30032  eleclclwwlknlem2  30036  umgr2cwwk2dif  30039  eleclclwwlkn  30051  hashecclwwlkn1  30052  umgrhashecclwwlk  30053  clwwlknonwwlknonb  30081  clwwlknonex2lem2  30083  clwwlknonex2  30084  1pthon2v  30128  upgr3v3e3cycl  30155  uhgr3cyclexlem  30156  uhgr3cyclex  30157  eupth2lem3lem4  30206  frgr3vlem1  30248  frgr3vlem2  30249  3vfriswmgrlem  30252  3vfriswmgr  30253  3cyclfrgrrn1  30260  n4cyclfrgr  30266  frgrncvvdeqlem3  30276  frgrncvvdeqlem6  30279  frgrncvvdeqlem7  30280  frgrncvvdeqlem8  30281  frgrwopreglem4a  30285  frgrwopreglem3  30289  frgrwopreg1  30293  frgrwopreg2  30294  frgrwopreglem5lem  30295  frgrwopreglem5ALT  30297  frgrwopreg  30298  fusgr2wsp2nb  30309  2wspmdisj  30312  numclwwlk1lem2foa  30329  numclwwlk1lem2f1  30332  numclwwlk1lem2fo  30333  numclwwlk1  30336  wlkl0  30342  numclwwlk2lem1  30351  numclwlk2lem2f  30352  numclwlk2lem2f1o  30354  frgrreg  30369  frgrregord013  30370  frgrregord13  30371  friendshipgt3  30373  friendship  30374  eulplig  30460  ipassi  30816  ubthlem2  30846  isch3  31216  shintcli  31304  shmodsi  31364  spansncvi  31627  hoaddsub  31791  eigorthi  31812  pjss2coi  32139  pjnormssi  32143  pj3cor1i  32184  strb  32233  dmdmd  32275  mdsl0  32285  csmdsymi  32309  chrelat2i  32340  mdsymlem3  32380  mdsymlem6  32383  sumdmdlem2  32394  opreu2reuALT  32451  ssrelf  32593  gsumwun  33040  trssfir1omregs  35120  onvf1odlem4  35138  spthcycl  35161  loop1cycl  35169  cvmlift2lem1  35334  satfrel  35399  satfrnmapom  35402  fmlafvel  35417  fmla1  35419  gonarlem  35426  gonar  35427  goalrlem  35428  goalr  35429  satffunlem  35433  satffunlem1lem1  35434  satffunlem2lem1  35436  satffun  35441  satefvfmla1  35457  mrsubvrs  35554  mclsax  35601  3ccased  35751  dfon2lem3  35818  rdgprc  35827  cgrextend  36041  btwndiff  36060  btwnconn1lem12  36131  brsegle  36141  broutsideof2  36155  funray  36173  in-ax8  36257  ss-ax8  36258  elicc3  36350  nn0prpwlem  36355  nn0prpw  36356  fnessref  36390  neibastop2lem  36393  filnetlem4  36414  meran1  36444  waj-ax  36447  arg-ax  36449  bj-nnclavc  36581  bj-con2com  36594  bj-axdd2  36625  bj-alrimg  36652  bj-exlimg  36656  bj-exalimi  36666  bj-cbvalimt  36672  bj-eximcom  36676  bj-ssbid1ALT  36698  bj-sb  36720  bj-snsetex  36996  bj-restpw  37125  bj-finsumval0  37318  mptsnunlem  37371  icoreclin  37390  relowlpssretop  37397  inunissunidif  37408  rdgssun  37411  finorwe  37415  domalom  37437  wl-dral1d  37564  wl-exeq  37567  wl-lem-exsb  37599  poimirlem29  37688  poimirlem32  37691  fdc  37784  seqpo  37786  incsequz  37787  isismty  37840  ismtybndlem  37845  heibor1lem  37848  ismgmOLD  37889  isexid2  37894  ghomco  37930  pridlc  38110  relcnveq3  38354  elrelscnveq3  38527  cdleme18d  40333  tendovalco  40803  cdlemn11pre  41248  dihord2pre  41263  indstrd  42225  unitscyglem3  42229  nnadddir  42302  eu6w  42708  incssnn0  42743  fphpd  42848  jm2.19lem3  43023  setindtr  43056  islssfg2  43103  mpaaeu  43182  ordnexbtwnsuc  43299  oaabsb  43326  succlg  43360  oacl2g  43362  omabs2  43364  omcl2  43365  omcl3g  43366  pr2cv  43580  refimssco  43639  iunrelexpmin1  43740  iunrelexpmin2  43744  trclimalb2  43758  clsk1indlem3  44075  tfindsd  44242  mnurndlem1  44313  nzss  44349  sb5ALT  44557  truniALT  44573  ee223  44666  3orbi123VD  44881  sbc3orgVD  44882  exbirVD  44884  exbiriVD  44885  sbcim2gVD  44906  trsbcVD  44908  truniALTVD  44909  onfrALTlem3VD  44918  onfrALTlem2VD  44920  csbrngVD  44927  19.41rgVD  44933  ax6e2eqVD  44938  ax6e2ndeqVD  44940  2uasbanhVD  44942  sb5ALTVD  44944  vk15.4jVD  44945  infxrunb3rnmpt  45465  stoweidlem26  46063  et-equeucl  46909  hirstL-ax3  46922  rexsb  47129  rexrsb  47130  euoreqb  47139  2reu8i  47143  afvres  47202  tz6.12-afv  47203  afvco2  47206  afv2orxorb  47258  afv2res  47269  tz6.12-afv2  47270  tz6.12i-afv2  47273  dfatcolem  47285  zm1nn  47332  2ffzoeq  47357  smonoord  47401  iccpartiltu  47452  iccpartlt  47454  iccpartltu  47455  iccpartgtl  47456  iccpartgt  47457  iccpartleu  47458  iccpartgel  47459  icceuelpart  47466  iccpartnel  47468  lswn0  47474  ichnreuop  47502  ichreuopeq  47503  prsprel  47517  sprsymrelfvlem  47520  sprsymrelf1lem  47521  sprsymrelfolem2  47523  prproropf1olem4  47536  paireqne  47541  prprelb  47546  reupr  47552  goldbachth  47577  odz2prm2pw  47593  fmtno4prmfac  47602  fmtno4prmfac193  47603  prmdvdsfmtnof1lem2  47615  2pwp1prmfmtno  47620  lighneallem2  47636  lighneallem4b  47639  lighneallem4  47640  requad2  47653  odd2prm2  47748  mogoldbblem  47750  gbepos  47788  gbowgt5  47792  gbowge7  47793  stgoldbwt  47806  sbgoldbwt  47807  sbgoldbst  47808  sbgoldbaltlem1  47809  sbgoldbalt  47811  sbgoldbo  47817  nnsum3primesle9  47824  nnsum4primesodd  47826  nnsum4primesoddALTV  47827  nnsum4primeseven  47830  nnsum4primesevenALTV  47831  bgoldbtbndlem1  47835  bgoldbtbndlem2  47836  bgoldbtbndlem3  47837  bgoldbtbnd  47839  dfnbgr6  47887  isuspgrimlem  47925  uhgrimisgrgric  47961  clnbgrgrim  47964  usgrgrtrirex  47980  isubgr3stgrlem4  47999  grilcbri2  48041  grlicsym  48043  grlictr  48045  gricgrlic  48048  gpgvtxedg0  48093  gpgvtxedg1  48094  gpgedg2ov  48096  gpgedg2iv  48097  pgnioedg1  48138  pgnioedg2  48139  pgnioedg3  48140  pgnioedg4  48141  pgnioedg5  48142  pgnbgreunbgrlem2lem3  48146  pgnbgreunbgrlem3  48148  pgnbgreunbgrlem5lem1  48150  pgnbgreunbgrlem5lem2  48151  pgnbgreunbgrlem5lem3  48152  pgnbgreunbgrlem6  48154  upgrwlkupwlk  48170  uspgrsprf1  48177  lmod0rng  48259  lidldomn1  48261  rngccatidALTV  48302  rngcinvALTV  48306  rhmsubcALTVlem4  48314  funcringcsetcALTV2lem9  48328  ringccatidALTV  48336  ringcbasbasALTV  48342  ztprmneprm  48377  pgrpgt2nabl  48396  lmodvsmdi  48409  ply1mulgsumlem2  48418  lincsumcl  48462  ellcoellss  48466  linindslinci  48479  islinindfis  48480  lincext3  48487  lindslinindimp2lem4  48492  lindslinindsimp2lem5  48493  lindslinindsimp2  48494  lindsrng01  48499  ldepspr  48504  lincresunit3lem1  48510  elfzolborelfzop1  48550  dignn0ldlem  48633  nn0sumshdiglem1  48652  1arymaptf1  48673  2arymaptf1  48684  rrx2xpref1o  48749  rrx2plord2  48753  rrx2plordisom  48754  line2ylem  48782  line2xlem  48784  line2y  48786  itschlc0xyqsol1  48797  inlinecirc02plem  48817  fullthinc  49481  tfis2d  49711  onsetrec  49739