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  2315  cbv1v  2334  exsb  2357  cbv1  2400  ax12b  2422  axc11n  2424  dvelimdf  2447  equvel  2454  dfsb1  2479  sbied  2501  dfmoeu  2529  mo3  2557  mo4  2559  2mo  2641  2eu6  2650  exists2  2655  pm2.61dne  3011  rexlimdv  3128  r19.21v  3154  r19.12  3278  2gencl  3479  3gencl  3480  vtocl2ga  3533  vtocl2gaf  3534  vtocl3gaf  3536  vtocl3ga  3538  vtocl4ga  3541  rspccv  3574  ceqex  3607  mob  3677  euind  3684  reuind  3713  2reu1  3849  sseq2  3962  nelss  4001  rexdifi  4101  reupick2  4282  disjeq0  4407  uneqdifeq  4444  sspw  4562  ssprsseq  4776  preq12b  4801  prnebg  4807  prel12g  4815  3elpr2eq  4857  iinss2  5006  trintss  5217  dtruALT2  5309  reusv2lem1  5337  alxfr  5346  ralxfrALT  5354  exexneq  5378  copsexgw  5433  copsexg  5434  snopeqop  5449  propeqop  5450  opthhausdorff  5460  opthhausdorff0  5461  pofun  5545  solin  5554  frss  5583  2optocl  5715  3optocl  5716  ssrel  5726  ssrel2  5728  ssrelrel  5739  relop  5793  dfres3  5935  asymref2  6066  xpidtr  6071  trin2  6072  poltletr  6081  imadifssran  6100  xp11  6124  relcnvtrg  6215  reuop  6241  tz7.7  6333  ordtr2  6352  suc11  6416  fundif  6531  fss  6668  f0dom0  6708  fv3  6840  tz6.12i  6848  mpteqb  6949  fveqdmss  7012  eldmrexrnb  7026  funopsn  7082  funsndifnop  7085  tpres  7137  funfvima  7166  fvclss  7177  f1veqaeq  7193  fvf1pr  7244  isoselem  7278  oprabv  7409  ovg  7514  elovmpt3rab1  7609  sorpsscmpl  7670  iunpw  7707  trom  7808  limom  7815  peano5  7826  focdmex  7891  funelss  7982  funeldmdif  7983  bropopvvv  8023  bropfvvvvlem  8024  f1o2ndf1  8055  poxp  8061  soxp  8062  poxp2  8076  frxp2  8077  frxp3  8084  suppimacnv  8107  ressuppss  8116  ressuppssdif  8118  tposfn2  8181  wfr3g  8252  onnseq  8267  smoel  8283  smogt  8290  smoiso2  8292  tfr3  8321  tz7.48-2  8364  tz7.48-3  8366  tz7.49  8367  oecl  8455  oaordex  8476  oalimcl  8478  oaass  8479  omordi  8484  omlimcl  8496  odi  8497  omeulem1  8500  oen0  8504  nnawordi  8539  nnaass  8540  nnmordi  8549  omabs  8569  omsmolem  8575  naddssim  8603  brinxper  8654  iiner  8716  2ecoptocl  8735  3ecoptocl  8736  undifixp  8861  xpdom2  8989  xpf1o  9056  infensuc  9072  findcard2  9078  php  9121  isinf  9154  unblem2  9182  fodomfir  9218  infssuni  9236  finsschain  9249  fsuppunfi  9278  fsuppunbi  9279  marypha1  9324  hartogs  9436  card2on  9446  card2inf  9447  xpwdomg  9477  elirrv  9489  elirrvOLD  9490  en3lp  9510  preleqg  9511  inf3lem1  9524  inf3lem2  9525  inf3lem3  9526  inf3lem5  9528  noinfep  9556  ttrclss  9616  ttrclselem2  9622  trcl  9624  tcel  9641  frr3g  9652  rankonidlem  9724  scottex  9781  djuunxp  9817  eldju2ndl  9820  updjud  9830  dif1card  9904  fodomnum  9951  cardaleph  9983  kmlem9  10053  kmlem13  10057  cflim2  10157  cfsmolem  10164  infpssrlem3  10199  isfin7-2  10290  fin1a2lem6  10299  fin1a2lem12  10305  domtriomlem  10336  axdc3lem4  10347  axdc4lem  10349  zorn2lem3  10392  zorn2lem4  10393  zorn2lem5  10394  zorn2lem7  10396  zornn0g  10399  axdclem2  10414  ondomon  10457  alephval2  10466  cfpwsdom  10478  wuncval2  10641  grupr  10691  gruiun  10693  ingru  10709  grothomex  10723  indpi  10801  nqereu  10823  prlem934  10927  reclem2pr  10942  mulgt0sr  10999  supsrlem  11005  1re  11115  dedekind  11279  lemul1a  11978  squeeze0  12028  peano5nni  12131  nnunb  12380  nn0lt2  12539  nn0le2is012  12540  fzind  12574  nn0ind-raph  12576  zindd  12577  eluzaddOLD  12770  uzin  12775  nn01to3  12842  xnn0xadd0  13149  xmulasslem  13187  icoshft  13376  fzen  13444  uzsubsubfz  13449  elfz0ubfz0  13535  elfz0fzfz0  13536  fz0fzelfz0  13537  elfzmlbp  13542  elfzodifsumelfzo  13634  ssfzo12bi  13664  fzoopth  13665  elfzonelfzo  13672  elfznelfzo  13675  injresinjlem  13690  injresinj  13691  modfzo0difsn  13850  modsumfzodifsn  13851  addmodlteq  13853  ssnn0fi  13892  fsuppmapnn0fiub0  13900  expcllem  13979  expeq0  13999  mulexp  14008  leexp2r  14081  bernneq  14136  facdiv  14194  hasheqf1oi  14258  hashnn0n0nn  14298  hashss  14316  hashgt12el  14329  hashgt12el2  14330  hashimarni  14348  hashle2pr  14384  pr2pwpr  14386  hashge2el2dif  14387  hashge2el2difr  14388  hashtpg  14392  hashge3el3dif  14394  exprelprel  14397  hash1to3  14399  hash3tpde  14400  tpfo  14407  fundmge2nop0  14409  fi1uzind  14414  ccatsymb  14489  swrdnd  14561  swrdnd2  14562  swrdnnn0nd  14563  swrdnd0  14564  pfxnd0  14595  swrdswrdlem  14610  swrdswrd  14611  pfxccatin12lem2a  14633  pfxccatin12lem1  14634  swrdccatin2  14635  pfxccatin12lem2  14637  pfxccatin12lem3  14638  pfxccat3  14640  swrdccat  14641  swrdccat3blem  14645  repsdf2  14684  repswswrd  14690  cshwidxmod  14709  cshwidx0  14712  cshf1  14716  cshweqrep  14727  cshw1  14728  cshwsexaOLD  14731  2cshwcshw  14732  scshwfzeqfzo  14733  cshwcsh2id  14735  wwlktovfo  14865  relexpaddg  14960  iseraltlem2  15590  modfsummods  15700  clim2prod  15795  prodfn0  15801  prodfrec  15802  prodmo  15843  fprodabs  15881  binomfallfac  15948  fprodefsum  16002  dvdsaddre2b  16218  addmodlteqALT  16236  oddge22np1  16260  nn0enne  16288  nn0o1gt2  16292  sumeven  16298  sumodd  16299  dvdslegcd  16415  gcdneg  16433  dfgcd2  16457  rplpwr  16469  lcmf  16544  lcmftp  16547  lcmfunsnlem2lem1  16549  lcmfunsnlem2  16551  lcmfdvdsb  16554  coprmdvds1  16563  qredeq  16568  coprmprod  16572  coprmproddvdslem  16573  cncongr1  16578  cncongr2  16579  prm2orodd  16602  2mulprm  16604  nnnn0modprm0  16718  prm23lt5  16726  prm23ge5  16727  dvdsprmpweqnn  16797  dvdsprmpweqle  16798  oddprmdvds  16815  prmpwdvds  16816  prmreclem4  16831  ramcl  16941  prmgaplem6  16968  prmgaplem7  16969  prmgaplem8  16970  cshwshashlem1  17007  cshwshashlem2  17008  cshwshashlem3  17009  cshwrepswhash1  17014  setsn0fun  17084  setsstruct2  17085  imasleval  17445  mreiincl  17498  mreexexd  17554  inveq  17681  cicsym  17711  cictr  17712  initoid  17908  termoid  17909  initoeu2lem0  17920  initoeu2lem1  17921  initoeu2lem2  17922  initoeu2  17923  fthestrcsetc  18056  fthsetcestrc  18071  drsdirfi  18211  isnmgm  18518  mgmhmlin  18573  issubmgm2  18577  sgrpass  18599  insubm  18692  mgm2nsgrplem3  18794  dfgrp3lem  18917  cyccom  19082  symg2bas  19272  symgfix2  19295  symgextf1  19300  gsmsymgrfix  19307  pmtrprfv3  19333  psgnunilem4  19376  efgi2  19604  0ringnnzr  20410  rnghmsscmap  20515  rnghmsubcsetclem2  20517  rngcinv  20522  funcrngcsetc  20525  funcrngcsetcALT  20526  rhmsscmap  20544  rhmsubcsetclem2  20546  rhmsubcrngclem2  20552  ringcbasbas  20558  funcringcsetc  20559  rhmsubclem4  20573  rngqiprngimfo  21208  psgndiflemB  21507  psgndiflemA  21508  elfrlmbasn0  21670  lmictra  21752  mpfrcl  21990  gsummoncoe1  22193  mamufacex  22281  matecl  22310  dmatelnd  22381  dmatscmcl  22388  scmateALT  22397  scmatsgrp1  22407  scmatf1  22416  mavmulsolcl  22436  cramerimplem1  22568  cramerimplem2  22569  pmatcollpw3fi1  22673  mp2pm2mplem4  22694  pm2mpfo  22699  chmaidscmat  22733  fvmptnn04ifb  22736  chfacfscmul0  22743  chfacfpmmul0  22747  cayhamlem1  22751  cayhamlem3  22772  cayleyhamilton1  22777  fiinopn  22786  tgcl  22854  distop  22880  isclo2  22973  iscldtop  22980  ssnei2  23001  opnnei  23005  pnfnei  23105  mnfnei  23106  tgcnp  23138  cnpnei  23149  1stcelcls  23346  txcnpi  23493  cnmptcom  23563  fbfinnfr  23726  isfildlem  23742  snfil  23749  fbunfip  23754  fgcl  23763  elfm2  23833  fmco  23846  fbflim2  23862  cnpflf2  23885  flimfcls  23911  tmdgsum  23980  neibl  24387  tngngpim  24545  fgcfil  25169  caubl  25206  volsuplem  25454  ellimc3  25778  dvnadd  25829  dvnres  25831  cpnord  25835  dvnfre  25854  ply1divex  26040  cxpmul2  26596  fsumdvdsmul  27103  zabsle1  27205  gausslemma2dlem1a  27274  gausslemma2dlem3  27277  lgsquad2lem2  27294  2lgs  27316  2sq2  27342  2sqnn0  27347  2sqnn  27348  2sqreultlem  27356  2sqreunnltlem  27359  qabvexp  27535  sltval2  27566  nolt02o  27605  ssltun1  27719  scutun12  27721  madebday  27814  mulsprop  28038  precsexlem8  28121  precsexlem9  28122  noseqind  28191  om2noseqrdg  28203  n0cutlt  28254  peano5uzs  28297  expadds  28327  axcontlem4  28912  umgredgprv  29052  umgrnloop  29053  upgrpredgv  29084  upgredgpr  29087  edglnl  29088  usgredgprvALT  29140  usgrnloopALT  29148  usgredg2v  29172  fusgrfis  29275  nbuhgr2vtx1edgblem  29296  nb3grprlem1  29325  cusgrsize2inds  29399  cusgrfi  29404  fusgrn0degnn0  29445  uspgrloopvtxel  29462  vtxdginducedm1lem4  29488  uhgr0edg0rgrb  29520  wlkl1loop  29583  wlk1walk  29584  upgriswlk  29586  upgrwlkvtxedg  29590  uspgr2wlkeq  29591  wlkv0  29595  wlksoneq1eq2  29608  wlkon2n0  29610  wlkreslem  29613  wlkres  29614  lfgrwlkprop  29631  pthdivtx  29672  2pthnloop  29676  spthonepeq  29697  uhgrwkspthlem2  29699  uhgrwkspth  29700  usgr2wlkneq  29701  usgr2trlncl  29705  usgr2pthlem  29708  usgr2pth  29709  cyclnspth  29746  lfgrn1cycl  29750  usgr2trlncrct  29751  uspgrn2crct  29753  crctcshwlkn0lem3  29757  crctcshwlkn0lem5  29759  wwlknp  29788  wspthneq1eq2  29805  0enwwlksnge1  29809  wlklnwwlkln1  29813  wlkiswwlks2  29820  wlkiswwlksupgr2  29822  wlklnwwlkln2lem  29827  wwlksnred  29837  wwlksnextbi  29839  wwlksnredwwlkn0  29841  wwlksnextwrd  29842  wwlksnextinj  29844  wwlksnextproplem3  29856  wwlksnextprop  29857  wspthsnwspthsnon  29861  wspthsnonn0vne  29862  2pthon3v  29888  umgr2adedgwlkonALT  29892  umgr2wlk  29894  umgr2wlkon  29895  umgrwwlks2on  29902  elwspths2on  29905  usgr2wspthons3  29909  elwwlks2  29911  rusgrnumwwlk  29920  clwwlkccatlem  29933  clwlkclwwlklem2a4  29941  clwlkclwwlklem2a  29942  clwlkclwwlklem2  29944  clwlkclwwlkf1lem3  29950  erclwwlkeqlen  29963  clwwlknwwlksn  29982  loopclwwlkn1b  29986  clwwlkf1  29993  wwlksext2clwwlk  30001  eleclclwwlknlem2  30005  umgr2cwwk2dif  30008  eleclclwwlkn  30020  hashecclwwlkn1  30021  umgrhashecclwwlk  30022  clwwlknonwwlknonb  30050  clwwlknonex2lem2  30052  clwwlknonex2  30053  1pthon2v  30097  upgr3v3e3cycl  30124  uhgr3cyclexlem  30125  uhgr3cyclex  30126  eupth2lem3lem4  30175  frgr3vlem1  30217  frgr3vlem2  30218  3vfriswmgrlem  30221  3vfriswmgr  30222  3cyclfrgrrn1  30229  n4cyclfrgr  30235  frgrncvvdeqlem3  30245  frgrncvvdeqlem6  30248  frgrncvvdeqlem7  30249  frgrncvvdeqlem8  30250  frgrwopreglem4a  30254  frgrwopreglem3  30258  frgrwopreg1  30262  frgrwopreg2  30263  frgrwopreglem5lem  30264  frgrwopreglem5ALT  30266  frgrwopreg  30267  fusgr2wsp2nb  30278  2wspmdisj  30281  numclwwlk1lem2foa  30298  numclwwlk1lem2f1  30301  numclwwlk1lem2fo  30302  numclwwlk1  30305  wlkl0  30311  numclwwlk2lem1  30320  numclwlk2lem2f  30321  numclwlk2lem2f1o  30323  frgrreg  30338  frgrregord013  30339  frgrregord13  30340  friendshipgt3  30342  friendship  30343  eulplig  30429  ipassi  30785  ubthlem2  30815  isch3  31185  shintcli  31273  shmodsi  31333  spansncvi  31596  hoaddsub  31760  eigorthi  31781  pjss2coi  32108  pjnormssi  32112  pj3cor1i  32153  strb  32202  dmdmd  32244  mdsl0  32254  csmdsymi  32278  chrelat2i  32309  mdsymlem3  32349  mdsymlem6  32352  sumdmdlem2  32363  opreu2reuALT  32421  ssrelf  32560  gsumwun  33018  onvf1odlem4  35083  spthcycl  35106  loop1cycl  35114  cvmlift2lem1  35279  satfrel  35344  satfrnmapom  35347  fmlafvel  35362  fmla1  35364  gonarlem  35371  gonar  35372  goalrlem  35373  goalr  35374  satffunlem  35378  satffunlem1lem1  35379  satffunlem2lem1  35381  satffun  35386  satefvfmla1  35402  mrsubvrs  35499  mclsax  35546  3ccased  35696  dfon2lem3  35763  rdgprc  35772  cgrextend  35986  btwndiff  36005  btwnconn1lem12  36076  brsegle  36086  broutsideof2  36100  funray  36118  in-ax8  36202  ss-ax8  36203  elicc3  36295  nn0prpwlem  36300  nn0prpw  36301  fnessref  36335  neibastop2lem  36338  filnetlem4  36359  meran1  36389  waj-ax  36392  arg-ax  36394  bj-nnclavc  36526  bj-con2com  36539  bj-axdd2  36570  bj-alrimg  36597  bj-exlimg  36601  bj-exalimi  36611  bj-cbvalimt  36617  bj-eximcom  36621  bj-ssbid1ALT  36643  bj-sb  36665  bj-snsetex  36941  bj-restpw  37070  bj-finsumval0  37263  mptsnunlem  37316  icoreclin  37335  relowlpssretop  37342  inunissunidif  37353  rdgssun  37356  finorwe  37360  domalom  37382  wl-dral1d  37509  wl-exeq  37512  wl-lem-exsb  37544  poimirlem29  37633  poimirlem32  37636  fdc  37729  seqpo  37731  incsequz  37732  isismty  37785  ismtybndlem  37790  heibor1lem  37793  ismgmOLD  37834  isexid2  37839  ghomco  37875  pridlc  38055  relcnveq3  38299  elrelscnveq3  38472  cdleme18d  40278  tendovalco  40748  cdlemn11pre  41193  dihord2pre  41208  indstrd  42170  unitscyglem3  42174  nnadddir  42247  eu6w  42653  incssnn0  42688  fphpd  42793  jm2.19lem3  42968  setindtr  43001  islssfg2  43048  mpaaeu  43127  ordnexbtwnsuc  43244  oaabsb  43271  succlg  43305  oacl2g  43307  omabs2  43309  omcl2  43310  omcl3g  43311  pr2cv  43525  refimssco  43584  iunrelexpmin1  43685  iunrelexpmin2  43689  trclimalb2  43703  clsk1indlem3  44020  tfindsd  44187  mnurndlem1  44258  nzss  44294  sb5ALT  44503  truniALT  44519  ee223  44612  3orbi123VD  44827  sbc3orgVD  44828  exbirVD  44830  exbiriVD  44831  sbcim2gVD  44852  trsbcVD  44854  truniALTVD  44855  onfrALTlem3VD  44864  onfrALTlem2VD  44866  csbrngVD  44873  19.41rgVD  44879  ax6e2eqVD  44884  ax6e2ndeqVD  44886  2uasbanhVD  44888  sb5ALTVD  44890  vk15.4jVD  44891  infxrunb3rnmpt  45411  stoweidlem26  46011  et-equeucl  46857  hirstL-ax3  46880  rexsb  47087  rexrsb  47088  euoreqb  47097  2reu8i  47101  afvres  47160  tz6.12-afv  47161  afvco2  47164  afv2orxorb  47216  afv2res  47227  tz6.12-afv2  47228  tz6.12i-afv2  47231  dfatcolem  47243  zm1nn  47290  2ffzoeq  47315  smonoord  47359  iccpartiltu  47410  iccpartlt  47412  iccpartltu  47413  iccpartgtl  47414  iccpartgt  47415  iccpartleu  47416  iccpartgel  47417  icceuelpart  47424  iccpartnel  47426  lswn0  47432  ichnreuop  47460  ichreuopeq  47461  prsprel  47475  sprsymrelfvlem  47478  sprsymrelf1lem  47479  sprsymrelfolem2  47481  prproropf1olem4  47494  paireqne  47499  prprelb  47504  reupr  47510  goldbachth  47535  odz2prm2pw  47551  fmtno4prmfac  47560  fmtno4prmfac193  47561  prmdvdsfmtnof1lem2  47573  2pwp1prmfmtno  47578  lighneallem2  47594  lighneallem4b  47597  lighneallem4  47598  requad2  47611  odd2prm2  47706  mogoldbblem  47708  gbepos  47746  gbowgt5  47750  gbowge7  47751  stgoldbwt  47764  sbgoldbwt  47765  sbgoldbst  47766  sbgoldbaltlem1  47767  sbgoldbalt  47769  sbgoldbo  47775  nnsum3primesle9  47782  nnsum4primesodd  47784  nnsum4primesoddALTV  47785  nnsum4primeseven  47788  nnsum4primesevenALTV  47789  bgoldbtbndlem1  47793  bgoldbtbndlem2  47794  bgoldbtbndlem3  47795  bgoldbtbnd  47797  dfnbgr6  47845  isuspgrimlem  47883  uhgrimisgrgric  47919  clnbgrgrim  47922  usgrgrtrirex  47938  isubgr3stgrlem4  47957  grilcbri2  47999  grlicsym  48001  grlictr  48003  gricgrlic  48006  gpgvtxedg0  48051  gpgvtxedg1  48052  gpgedg2ov  48054  gpgedg2iv  48055  pgnioedg1  48096  pgnioedg2  48097  pgnioedg3  48098  pgnioedg4  48099  pgnioedg5  48100  pgnbgreunbgrlem2lem3  48104  pgnbgreunbgrlem3  48106  pgnbgreunbgrlem5lem1  48108  pgnbgreunbgrlem5lem2  48109  pgnbgreunbgrlem5lem3  48110  pgnbgreunbgrlem6  48112  upgrwlkupwlk  48128  uspgrsprf1  48135  lmod0rng  48217  lidldomn1  48219  rngccatidALTV  48260  rngcinvALTV  48264  rhmsubcALTVlem4  48272  funcringcsetcALTV2lem9  48286  ringccatidALTV  48294  ringcbasbasALTV  48300  ztprmneprm  48335  pgrpgt2nabl  48354  lmodvsmdi  48367  ply1mulgsumlem2  48376  lincsumcl  48420  ellcoellss  48424  linindslinci  48437  islinindfis  48438  lincext3  48445  lindslinindimp2lem4  48450  lindslinindsimp2lem5  48451  lindslinindsimp2  48452  lindsrng01  48457  ldepspr  48462  lincresunit3lem1  48468  elfzolborelfzop1  48508  dignn0ldlem  48591  nn0sumshdiglem1  48610  1arymaptf1  48631  2arymaptf1  48642  rrx2xpref1o  48707  rrx2plord2  48711  rrx2plordisom  48712  line2ylem  48740  line2xlem  48742  line2y  48744  itschlc0xyqsol1  48755  inlinecirc02plem  48775  fullthinc  49439  tfis2d  49669  onsetrec  49697