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  2187  sbiedw  2321  cbv1v  2340  exsb  2363  cbv1  2406  ax12b  2428  axc11n  2430  dvelimdf  2453  equvel  2460  dfsb1  2485  sbied  2507  dfmoeu  2535  mo3  2564  mo4  2566  2mo  2648  2eu6  2657  exists2  2662  pm2.61dne  3018  rexlimdv  3135  r19.21v  3161  r19.12  3285  2gencl  3483  3gencl  3484  vtocl2ga  3533  vtocl2gaf  3534  vtocl3gaf  3536  vtocl3ga  3538  vtocl4ga  3541  rspccv  3573  ceqex  3606  mob  3675  euind  3682  reuind  3711  2reu1  3847  sseq2  3960  nelss  3999  rexdifi  4102  reupick2  4283  disjeq0  4408  uneqdifeq  4445  sspw  4565  ssprsseq  4781  preq12b  4806  prnebg  4812  prel12g  4820  3elpr2eq  4862  iinss2  5013  trintss  5223  dtruALT2  5315  reusv2lem1  5343  alxfr  5352  ralxfrALT  5360  exexneq  5384  copsexgw  5438  copsexg  5439  snopeqop  5454  propeqop  5455  opthhausdorff  5465  opthhausdorff0  5466  pofun  5550  solin  5559  frss  5588  2optocl  5720  3optocl  5721  ssrel  5732  ssrel2  5734  ssrelrel  5745  relop  5799  dfres3  5943  asymref2  6074  xpidtr  6079  trin2  6080  poltletr  6089  imadifssran  6109  xp11  6133  relcnvtrg  6225  reuop  6251  tz7.7  6343  ordtr2  6362  suc11  6426  fundif  6541  fss  6678  f0dom0  6718  fv3  6852  tz6.12i  6860  mpteqb  6960  fveqdmss  7023  eldmrexrnb  7037  funopsn  7093  funsndifnop  7096  tpres  7147  funfvima  7176  fvclss  7187  f1veqaeq  7202  fvf1pr  7253  isoselem  7287  oprabv  7418  ovg  7523  elovmpt3rab1  7618  sorpsscmpl  7679  iunpw  7716  trom  7817  limom  7824  peano5  7835  focdmex  7900  funelss  7991  funeldmdif  7992  bropopvvv  8032  bropfvvvvlem  8033  f1o2ndf1  8064  poxp  8070  soxp  8071  poxp2  8085  frxp2  8086  frxp3  8093  suppimacnv  8116  ressuppss  8125  ressuppssdif  8127  tposfn2  8190  wfr3g  8261  onnseq  8276  smoel  8292  smogt  8299  smoiso2  8301  tfr3  8330  tz7.48-2  8373  tz7.48-3  8375  tz7.49  8376  oecl  8464  oaordex  8485  oalimcl  8487  oaass  8488  omordi  8493  omlimcl  8505  odi  8506  omeulem1  8509  oen0  8514  nnawordi  8549  nnaass  8550  nnmordi  8559  omabs  8579  omsmolem  8585  naddssim  8613  brinxper  8664  iiner  8726  2ecoptocl  8745  3ecoptocl  8746  undifixp  8872  xpdom2  9000  xpf1o  9067  infensuc  9083  findcard2  9089  php  9131  isinf  9165  unblem2  9193  fodomfir  9228  infssuni  9246  finsschain  9259  fsuppunfi  9291  fsuppunbi  9292  marypha1  9337  hartogs  9449  card2on  9459  card2inf  9460  xpwdomg  9490  elirrv  9502  elirrvOLD  9503  en3lp  9523  preleqg  9524  inf3lem1  9537  inf3lem2  9538  inf3lem3  9539  inf3lem5  9541  noinfep  9569  ttrclss  9629  ttrclselem2  9635  trcl  9637  tcel  9652  frr3g  9668  rankonidlem  9740  scottex  9797  djuunxp  9833  eldju2ndl  9836  updjud  9846  dif1card  9920  fodomnum  9967  cardaleph  9999  kmlem9  10069  kmlem13  10073  cflim2  10173  cfsmolem  10180  infpssrlem3  10215  isfin7-2  10306  fin1a2lem6  10315  fin1a2lem12  10321  domtriomlem  10352  axdc3lem4  10363  axdc4lem  10365  zorn2lem3  10408  zorn2lem4  10409  zorn2lem5  10410  zorn2lem7  10412  zornn0g  10415  axdclem2  10430  ondomon  10473  alephval2  10483  cfpwsdom  10495  wuncval2  10658  grupr  10708  gruiun  10710  ingru  10726  grothomex  10740  indpi  10818  nqereu  10840  prlem934  10944  reclem2pr  10959  mulgt0sr  11016  supsrlem  11022  1re  11132  dedekind  11296  lemul1a  11995  squeeze0  12045  peano5nni  12148  nnunb  12397  nn0lt2  12555  nn0le2is012  12556  fzind  12590  nn0ind-raph  12592  zindd  12593  uzin  12787  nn01to3  12854  xnn0xadd0  13162  xmulasslem  13200  icoshft  13389  fzen  13457  uzsubsubfz  13462  elfz0ubfz0  13548  elfz0fzfz0  13549  fz0fzelfz0  13550  elfzmlbp  13555  elfzodifsumelfzo  13647  ssfzo12bi  13677  fzoopth  13678  elfzonelfzo  13685  elfznelfzo  13689  injresinjlem  13706  injresinj  13707  modfzo0difsn  13866  modsumfzodifsn  13867  addmodlteq  13869  ssnn0fi  13908  fsuppmapnn0fiub0  13916  expcllem  13995  expeq0  14015  mulexp  14024  leexp2r  14097  bernneq  14152  facdiv  14210  hasheqf1oi  14274  hashnn0n0nn  14314  hashss  14332  hashgt12el  14345  hashgt12el2  14346  hashimarni  14364  hashle2pr  14400  pr2pwpr  14402  hashge2el2dif  14403  hashge2el2difr  14404  hashtpg  14408  hashge3el3dif  14410  exprelprel  14413  hash1to3  14415  hash3tpde  14416  tpfo  14423  fundmge2nop0  14425  fi1uzind  14430  ccatsymb  14506  swrdnd  14578  swrdnd2  14579  swrdnnn0nd  14580  swrdnd0  14581  pfxnd0  14612  swrdswrdlem  14627  swrdswrd  14628  pfxccatin12lem2a  14650  pfxccatin12lem1  14651  swrdccatin2  14652  pfxccatin12lem2  14654  pfxccatin12lem3  14655  pfxccat3  14657  swrdccat  14658  swrdccat3blem  14662  repsdf2  14701  repswswrd  14707  cshwidxmod  14726  cshwidx0  14729  cshf1  14733  cshweqrep  14744  cshw1  14745  2cshwcshw  14748  scshwfzeqfzo  14749  cshwcsh2id  14751  wwlktovfo  14881  relexpaddg  14976  iseraltlem2  15606  modfsummods  15716  clim2prod  15811  prodfn0  15817  prodfrec  15818  prodmo  15859  fprodabs  15897  binomfallfac  15964  fprodefsum  16018  dvdsaddre2b  16234  addmodlteqALT  16252  oddge22np1  16276  nn0enne  16304  nn0o1gt2  16308  sumeven  16314  sumodd  16315  dvdslegcd  16431  gcdneg  16449  dfgcd2  16473  rplpwr  16485  lcmf  16560  lcmftp  16563  lcmfunsnlem2lem1  16565  lcmfunsnlem2  16567  lcmfdvdsb  16570  coprmdvds1  16579  qredeq  16584  coprmprod  16588  coprmproddvdslem  16589  cncongr1  16594  cncongr2  16595  prm2orodd  16618  2mulprm  16620  nnnn0modprm0  16734  prm23lt5  16742  prm23ge5  16743  dvdsprmpweqnn  16813  dvdsprmpweqle  16814  oddprmdvds  16831  prmpwdvds  16832  prmreclem4  16847  ramcl  16957  prmgaplem6  16984  prmgaplem7  16985  prmgaplem8  16986  cshwshashlem1  17023  cshwshashlem2  17024  cshwshashlem3  17025  cshwrepswhash1  17030  setsn0fun  17100  setsstruct2  17101  imasleval  17462  mreiincl  17515  mreexexd  17571  inveq  17698  cicsym  17728  cictr  17729  initoid  17925  termoid  17926  initoeu2lem0  17937  initoeu2lem1  17938  initoeu2lem2  17939  initoeu2  17940  fthestrcsetc  18073  fthsetcestrc  18088  drsdirfi  18228  isnmgm  18569  mgmhmlin  18624  issubmgm2  18628  sgrpass  18650  insubm  18743  mgm2nsgrplem3  18845  dfgrp3lem  18968  cyccom  19132  symg2bas  19322  symgfix2  19345  symgextf1  19350  gsmsymgrfix  19357  pmtrprfv3  19383  psgnunilem4  19426  efgi2  19654  0ringnnzr  20458  rnghmsscmap  20563  rnghmsubcsetclem2  20565  rngcinv  20570  funcrngcsetc  20573  funcrngcsetcALT  20574  rhmsscmap  20592  rhmsubcsetclem2  20594  rhmsubcrngclem2  20600  ringcbasbas  20606  funcringcsetc  20607  rhmsubclem4  20621  rngqiprngimfo  21256  psgndiflemB  21555  psgndiflemA  21556  elfrlmbasn0  21718  lmictra  21800  mpfrcl  22040  gsummoncoe1  22252  mamufacex  22340  matecl  22369  dmatelnd  22440  dmatscmcl  22447  scmateALT  22456  scmatsgrp1  22466  scmatf1  22475  mavmulsolcl  22495  cramerimplem1  22627  cramerimplem2  22628  pmatcollpw3fi1  22732  mp2pm2mplem4  22753  pm2mpfo  22758  chmaidscmat  22792  fvmptnn04ifb  22795  chfacfscmul0  22802  chfacfpmmul0  22806  cayhamlem1  22810  cayhamlem3  22831  cayleyhamilton1  22836  fiinopn  22845  tgcl  22913  distop  22939  isclo2  23032  iscldtop  23039  ssnei2  23060  opnnei  23064  pnfnei  23164  mnfnei  23165  tgcnp  23197  cnpnei  23208  1stcelcls  23405  txcnpi  23552  cnmptcom  23622  fbfinnfr  23785  isfildlem  23801  snfil  23808  fbunfip  23813  fgcl  23822  elfm2  23892  fmco  23905  fbflim2  23921  cnpflf2  23944  flimfcls  23970  tmdgsum  24039  neibl  24445  tngngpim  24603  fgcfil  25227  caubl  25264  volsuplem  25512  ellimc3  25836  dvnadd  25887  dvnres  25889  cpnord  25893  dvnfre  25912  ply1divex  26098  cxpmul2  26654  fsumdvdsmul  27161  zabsle1  27263  gausslemma2dlem1a  27332  gausslemma2dlem3  27335  lgsquad2lem2  27352  2lgs  27374  2sq2  27400  2sqnn0  27405  2sqnn  27406  2sqreultlem  27414  2sqreunnltlem  27417  qabvexp  27593  ltsval2  27624  nolt02o  27663  sltsun1  27784  cutsun12  27786  madebday  27896  mulsprop  28126  precsexlem8  28210  precsexlem9  28211  noseqind  28288  om2noseqrdg  28300  n0cutlt  28355  peano5uzs  28400  expadds  28431  bdaypw2n0bndlem  28459  bdaypw2n0bnd  28460  axcontlem4  29040  umgredgprv  29180  umgrnloop  29181  upgrpredgv  29212  upgredgpr  29215  edglnl  29216  usgredgprvALT  29268  usgrnloopALT  29276  usgredg2v  29300  fusgrfis  29403  nbuhgr2vtx1edgblem  29424  nb3grprlem1  29453  cusgrsize2inds  29527  cusgrfi  29532  fusgrn0degnn0  29573  uspgrloopvtxel  29590  vtxdginducedm1lem4  29616  uhgr0edg0rgrb  29648  wlkl1loop  29711  wlk1walk  29712  upgriswlk  29714  upgrwlkvtxedg  29718  uspgr2wlkeq  29719  wlkv0  29723  wlksoneq1eq2  29736  wlkon2n0  29738  wlkreslem  29741  wlkres  29742  lfgrwlkprop  29759  pthdivtx  29800  2pthnloop  29804  spthonepeq  29825  uhgrwkspthlem2  29827  uhgrwkspth  29828  usgr2wlkneq  29829  usgr2trlncl  29833  usgr2pthlem  29836  usgr2pth  29837  cyclnspth  29874  lfgrn1cycl  29878  usgr2trlncrct  29879  uspgrn2crct  29881  crctcshwlkn0lem3  29885  crctcshwlkn0lem5  29887  wwlknp  29916  wspthneq1eq2  29933  0enwwlksnge1  29937  wlklnwwlkln1  29941  wlkiswwlks2  29948  wlkiswwlksupgr2  29950  wlklnwwlkln2lem  29955  wwlksnred  29965  wwlksnextbi  29967  wwlksnredwwlkn0  29969  wwlksnextwrd  29970  wwlksnextinj  29972  wwlksnextproplem3  29984  wwlksnextprop  29985  wspthsnwspthsnon  29989  wspthsnonn0vne  29990  2pthon3v  30016  umgr2adedgwlkonALT  30020  umgr2wlk  30022  umgr2wlkon  30023  usgrwwlks2on  30031  umgrwwlks2on  30032  elwspths2on  30035  elwspths2onw  30036  usgr2wspthons3  30040  elwwlks2  30042  rusgrnumwwlk  30051  clwwlkccatlem  30064  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  clwlkclwwlklem2  30075  clwlkclwwlkf1lem3  30081  erclwwlkeqlen  30094  clwwlknwwlksn  30113  loopclwwlkn1b  30117  clwwlkf1  30124  wwlksext2clwwlk  30132  eleclclwwlknlem2  30136  umgr2cwwk2dif  30139  eleclclwwlkn  30151  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  clwwlknonwwlknonb  30181  clwwlknonex2lem2  30183  clwwlknonex2  30184  1pthon2v  30228  upgr3v3e3cycl  30255  uhgr3cyclexlem  30256  uhgr3cyclex  30257  eupth2lem3lem4  30306  frgr3vlem1  30348  frgr3vlem2  30349  3vfriswmgrlem  30352  3vfriswmgr  30353  3cyclfrgrrn1  30360  n4cyclfrgr  30366  frgrncvvdeqlem3  30376  frgrncvvdeqlem6  30379  frgrncvvdeqlem7  30380  frgrncvvdeqlem8  30381  frgrwopreglem4a  30385  frgrwopreglem3  30389  frgrwopreg1  30393  frgrwopreg2  30394  frgrwopreglem5lem  30395  frgrwopreglem5ALT  30397  frgrwopreg  30398  fusgr2wsp2nb  30409  2wspmdisj  30412  numclwwlk1lem2foa  30429  numclwwlk1lem2f1  30432  numclwwlk1lem2fo  30433  numclwwlk1  30436  wlkl0  30442  numclwwlk2lem1  30451  numclwlk2lem2f  30452  numclwlk2lem2f1o  30454  frgrreg  30469  frgrregord013  30470  frgrregord13  30471  friendshipgt3  30473  friendship  30474  eulplig  30560  ipassi  30916  ubthlem2  30946  isch3  31316  shintcli  31404  shmodsi  31464  spansncvi  31727  hoaddsub  31891  eigorthi  31912  pjss2coi  32239  pjnormssi  32243  pj3cor1i  32284  strb  32333  dmdmd  32375  mdsl0  32385  csmdsymi  32409  chrelat2i  32440  mdsymlem3  32480  mdsymlem6  32483  sumdmdlem2  32494  opreu2reuALT  32551  ssrelf  32693  gsumwun  33158  r1filim  35260  trssfir1om  35267  fineqvinfep  35281  trssfir1omregs  35292  onvf1odlem4  35300  spthcycl  35323  loop1cycl  35331  cvmlift2lem1  35496  satfrel  35561  satfrnmapom  35564  fmlafvel  35579  fmla1  35581  gonarlem  35588  gonar  35589  goalrlem  35590  goalr  35591  satffunlem  35595  satffunlem1lem1  35596  satffunlem2lem1  35598  satffun  35603  satefvfmla1  35619  mrsubvrs  35716  mclsax  35763  3ccased  35913  dfon2lem3  35977  rdgprc  35986  cgrextend  36202  btwndiff  36221  btwnconn1lem12  36292  brsegle  36302  broutsideof2  36316  funray  36334  in-ax8  36418  ss-ax8  36419  elicc3  36511  nn0prpwlem  36516  nn0prpw  36517  fnessref  36551  neibastop2lem  36554  filnetlem4  36575  meran1  36605  waj-ax  36608  arg-ax  36610  bj-nnclavc  36748  bj-con2com  36761  bj-axdd2  36792  bj-alrimg  36819  bj-exlimg  36823  bj-exalimi  36833  bj-cbvalimt  36839  bj-eximcom  36843  bj-ssbid1ALT  36866  bj-sb  36888  bj-snsetex  37164  bj-restpw  37293  bj-finsumval0  37486  mptsnunlem  37539  icoreclin  37558  relowlpssretop  37565  inunissunidif  37576  rdgssun  37579  finorwe  37583  domalom  37605  wl-dral1d  37732  wl-exeq  37735  wl-lem-exsb  37767  wl-eujustlem1  37789  poimirlem29  37846  poimirlem32  37849  fdc  37942  seqpo  37944  incsequz  37945  isismty  37998  ismtybndlem  38003  heibor1lem  38006  ismgmOLD  38047  isexid2  38052  ghomco  38088  pridlc  38268  relcnveq3  38516  elrelscnveq3  38796  cdleme18d  40551  tendovalco  41021  cdlemn11pre  41466  dihord2pre  41481  indstrd  42443  unitscyglem3  42447  nnadddir  42521  eu6w  42915  incssnn0  42949  fphpd  43054  jm2.19lem3  43229  setindtr  43262  islssfg2  43309  mpaaeu  43388  ordnexbtwnsuc  43505  oaabsb  43532  succlg  43566  oacl2g  43568  omabs2  43570  omcl2  43571  omcl3g  43572  pr2cv  43785  refimssco  43844  iunrelexpmin1  43945  iunrelexpmin2  43949  trclimalb2  43963  clsk1indlem3  44280  tfindsd  44447  mnurndlem1  44518  nzss  44554  sb5ALT  44762  truniALT  44778  ee223  44871  3orbi123VD  45086  sbc3orgVD  45087  exbirVD  45089  exbiriVD  45090  sbcim2gVD  45111  trsbcVD  45113  truniALTVD  45114  onfrALTlem3VD  45123  onfrALTlem2VD  45125  csbrngVD  45132  19.41rgVD  45138  ax6e2eqVD  45143  ax6e2ndeqVD  45145  2uasbanhVD  45147  sb5ALTVD  45149  vk15.4jVD  45150  infxrunb3rnmpt  45668  stoweidlem26  46266  et-equeucl  47112  hirstL-ax3  47134  rexsb  47341  rexrsb  47342  euoreqb  47351  2reu8i  47355  afvres  47414  tz6.12-afv  47415  afvco2  47418  afv2orxorb  47470  afv2res  47481  tz6.12-afv2  47482  tz6.12i-afv2  47485  dfatcolem  47497  zm1nn  47544  2ffzoeq  47569  smonoord  47613  iccpartiltu  47664  iccpartlt  47666  iccpartltu  47667  iccpartgtl  47668  iccpartgt  47669  iccpartleu  47670  iccpartgel  47671  icceuelpart  47678  iccpartnel  47680  lswn0  47686  ichnreuop  47714  ichreuopeq  47715  prsprel  47729  sprsymrelfvlem  47732  sprsymrelf1lem  47733  sprsymrelfolem2  47735  prproropf1olem4  47748  paireqne  47753  prprelb  47758  reupr  47764  goldbachth  47789  odz2prm2pw  47805  fmtno4prmfac  47814  fmtno4prmfac193  47815  prmdvdsfmtnof1lem2  47827  2pwp1prmfmtno  47832  lighneallem2  47848  lighneallem4b  47851  lighneallem4  47852  requad2  47865  odd2prm2  47960  mogoldbblem  47962  gbepos  48000  gbowgt5  48004  gbowge7  48005  stgoldbwt  48018  sbgoldbwt  48019  sbgoldbst  48020  sbgoldbaltlem1  48021  sbgoldbalt  48023  sbgoldbo  48029  nnsum3primesle9  48036  nnsum4primesodd  48038  nnsum4primesoddALTV  48039  nnsum4primeseven  48042  nnsum4primesevenALTV  48043  bgoldbtbndlem1  48047  bgoldbtbndlem2  48048  bgoldbtbndlem3  48049  bgoldbtbnd  48051  dfnbgr6  48099  isuspgrimlem  48137  uhgrimisgrgric  48173  clnbgrgrim  48176  usgrgrtrirex  48192  isubgr3stgrlem4  48211  grilcbri2  48253  grlicsym  48255  grlictr  48257  gricgrlic  48260  gpgvtxedg0  48305  gpgvtxedg1  48306  gpgedg2ov  48308  gpgedg2iv  48309  pgnioedg1  48350  pgnioedg2  48351  pgnioedg3  48352  pgnioedg4  48353  pgnioedg5  48354  pgnbgreunbgrlem2lem3  48358  pgnbgreunbgrlem3  48360  pgnbgreunbgrlem5lem1  48362  pgnbgreunbgrlem5lem2  48363  pgnbgreunbgrlem5lem3  48364  pgnbgreunbgrlem6  48366  upgrwlkupwlk  48382  uspgrsprf1  48389  lmod0rng  48471  lidldomn1  48473  rngccatidALTV  48514  rngcinvALTV  48518  rhmsubcALTVlem4  48526  funcringcsetcALTV2lem9  48540  ringccatidALTV  48548  ringcbasbasALTV  48554  ztprmneprm  48589  pgrpgt2nabl  48608  lmodvsmdi  48621  ply1mulgsumlem2  48629  lincsumcl  48673  ellcoellss  48677  linindslinci  48690  islinindfis  48691  lincext3  48698  lindslinindimp2lem4  48703  lindslinindsimp2lem5  48704  lindslinindsimp2  48705  lindsrng01  48710  ldepspr  48715  lincresunit3lem1  48721  elfzolborelfzop1  48761  dignn0ldlem  48844  nn0sumshdiglem1  48863  1arymaptf1  48884  2arymaptf1  48895  rrx2xpref1o  48960  rrx2plord2  48964  rrx2plordisom  48965  line2ylem  48993  line2xlem  48995  line2y  48997  itschlc0xyqsol1  49008  inlinecirc02plem  49028  fullthinc  49691  tfis2d  49921  onsetrec  49949