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  840  jaod  858  orel1  887  pm2.62  898  pm2.75  932  pm2.64  942  ccased  1039  dedlem0b  1045  3impd  1348  3expd  1353  mp3an1i  1454  minimp  1619  meredith  1639  19.35  1876  speimfw  1963  equtrr  2021  equeucl  2023  ax12ev2  2181  sbiedw  2320  cbv1v  2342  exsb  2365  cbv1  2410  ax12b  2432  axc11n  2434  dvelimdf  2457  equvel  2464  dfsb1  2489  sbied  2511  dfmoeu  2539  mo3  2567  mo4  2569  2mo  2651  2eu6  2660  exists2  2665  pm2.61dne  3034  rexlimdv  3159  r19.21v  3186  r19.12  3320  r19.12OLD  3321  2gencl  3534  3gencl  3535  vtocl2ga  3590  vtocl2gaf  3591  vtocl3gaf  3593  vtocl3ga  3595  vtocl4ga  3599  rspccv  3632  ceqex  3665  mob  3739  euind  3746  reuind  3775  2reu1  3919  sseq2  4035  nelss  4074  rexdifi  4173  reupick2  4350  disjeq0  4479  uneqdifeq  4516  sspw  4633  ssprsseq  4850  preq12b  4875  prnebg  4880  prel12g  4888  3elpr2eq  4930  iinss2  5080  trintss  5302  dtruALT2  5388  reusv2lem1  5416  alxfr  5425  ralxfrALT  5433  exexneq  5454  dtruOLD  5461  copsexgw  5510  copsexg  5511  snopeqop  5525  propeqop  5526  opthhausdorff  5536  opthhausdorff0  5537  poclOLD  5616  pofun  5626  solin  5634  frss  5664  2optocl  5795  3optocl  5796  ssrel  5806  ssrelOLD  5807  ssrel2  5809  ssrelrel  5820  relop  5875  dfres3  6014  asymref2  6149  xpidtr  6154  trin2  6155  poltletr  6164  xp11  6206  relcnvtrg  6297  reuop  6324  tz7.7  6421  ordtr2  6439  suc11  6502  iotavalOLD  6547  funmoOLD  6594  fundif  6627  fss  6763  f0dom0  6805  fv3  6938  tz6.12i  6948  mpteqb  7048  fveqdmss  7112  eldmrexrnb  7126  funopsn  7182  funsndifnop  7185  tpres  7238  funfvima  7267  fvclss  7278  f1veqaeq  7294  fvf1pr  7343  isoselem  7377  oprabv  7510  ovg  7615  elovmpt3rab1  7710  sorpsscmpl  7769  iunpw  7806  trom  7912  limom  7919  peano5  7932  peano5OLD  7933  focdmex  7996  funelss  8088  funeldmdif  8089  bropopvvv  8131  bropfvvvvlem  8132  f1o2ndf1  8163  poxp  8169  soxp  8170  poxp2  8184  frxp2  8185  frxp3  8192  suppimacnv  8215  ressuppss  8224  ressuppssdif  8226  tposfn2  8289  wfr3g  8363  onnseq  8400  smoel  8416  smogt  8423  smoiso2  8425  tfr3  8455  tz7.48-2  8498  tz7.48-3  8500  tz7.49  8501  oecl  8593  oaordex  8614  oalimcl  8616  oaass  8617  omordi  8622  omlimcl  8634  odi  8635  omeulem1  8638  oen0  8642  nnawordi  8677  nnaass  8678  nnmordi  8687  omabs  8707  omsmolem  8713  naddssim  8741  brinxper  8792  iiner  8847  2ecoptocl  8866  3ecoptocl  8867  undifixp  8992  xpdom2  9133  xpf1o  9205  infensuc  9221  findcard2  9230  php  9273  phpOLD  9285  onomeneqOLD  9292  isinf  9323  isinfOLD  9324  unblem2  9357  fodomfir  9396  infssuni  9414  finsschain  9429  fsuppunfi  9457  fsuppunbi  9458  marypha1  9503  hartogs  9613  card2on  9623  card2inf  9624  xpwdomg  9654  elirrv  9665  en3lp  9683  preleqg  9684  inf3lem1  9697  inf3lem2  9698  inf3lem3  9699  inf3lem5  9701  noinfep  9729  ttrclss  9789  ttrclselem2  9795  trcl  9797  tcel  9814  frr3g  9825  rankonidlem  9897  scottex  9954  djuunxp  9990  eldju2ndl  9993  updjud  10003  dif1card  10079  fodomnum  10126  cardaleph  10158  kmlem9  10228  kmlem13  10232  cflim2  10332  cfsmolem  10339  infpssrlem3  10374  isfin7-2  10465  fin1a2lem6  10474  fin1a2lem12  10480  domtriomlem  10511  axdc3lem4  10522  axdc4lem  10524  zorn2lem3  10567  zorn2lem4  10568  zorn2lem5  10569  zorn2lem7  10571  zornn0g  10574  axdclem2  10589  ondomon  10632  alephval2  10641  cfpwsdom  10653  wuncval2  10816  grupr  10866  gruiun  10868  ingru  10884  grothomex  10898  indpi  10976  nqereu  10998  prlem934  11102  reclem2pr  11117  mulgt0sr  11174  supsrlem  11180  dedekind  11453  lemul1a  12148  squeeze0  12198  peano5nni  12296  nnunb  12549  nn0lt2  12706  nn0le2is012  12707  fzind  12741  nn0ind-raph  12743  zindd  12744  eluzaddOLD  12938  uzin  12943  nn01to3  13006  xnn0xadd0  13309  xmulasslem  13347  icoshft  13533  fzen  13601  uzsubsubfz  13606  elfz0ubfz0  13689  elfz0fzfz0  13690  fz0fzelfz0  13691  elfzmlbp  13696  elfzodifsumelfzo  13782  ssfzo12bi  13811  fzoopth  13812  elfzonelfzo  13819  elfznelfzo  13822  injresinjlem  13837  injresinj  13838  modfzo0difsn  13994  modsumfzodifsn  13995  addmodlteq  13997  ssnn0fi  14036  fsuppmapnn0fiub0  14044  expcllem  14123  expeq0  14143  mulexp  14152  leexp2r  14224  bernneq  14278  facdiv  14336  hasheqf1oi  14400  hashnn0n0nn  14440  hashss  14458  hashgt12el  14471  hashgt12el2  14472  hashimarni  14490  hashle2pr  14526  pr2pwpr  14528  hashge2el2dif  14529  hashge2el2difr  14530  hashtpg  14534  hashge3el3dif  14536  exprelprel  14539  hash1to3  14541  hash3tpde  14542  tpfo  14549  fundmge2nop0  14551  fi1uzind  14556  ccatsymb  14630  swrdnd  14702  swrdnd2  14703  swrdnnn0nd  14704  swrdnd0  14705  pfxnd0  14736  swrdswrdlem  14752  swrdswrd  14753  pfxccatin12lem2a  14775  pfxccatin12lem1  14776  swrdccatin2  14777  pfxccatin12lem2  14779  pfxccatin12lem3  14780  pfxccat3  14782  swrdccat  14783  swrdccat3blem  14787  repsdf2  14826  repswswrd  14832  cshwidxmod  14851  cshwidx0  14854  cshf1  14858  cshweqrep  14869  cshw1  14870  cshwsexaOLD  14873  2cshwcshw  14874  scshwfzeqfzo  14875  cshwcsh2id  14877  wwlktovfo  15007  relexpaddg  15102  iseraltlem2  15731  modfsummods  15841  clim2prod  15936  prodfn0  15942  prodfrec  15943  prodmo  15984  fprodabs  16022  binomfallfac  16089  fprodefsum  16143  dvdsaddre2b  16355  addmodlteqALT  16373  oddge22np1  16397  nn0enne  16425  nn0o1gt2  16429  sumeven  16435  sumodd  16436  dvdslegcd  16550  gcdneg  16568  dfgcd2  16593  rplpwr  16605  lcmf  16680  lcmftp  16683  lcmfunsnlem2lem1  16685  lcmfunsnlem2  16687  lcmfdvdsb  16690  coprmdvds1  16699  qredeq  16704  coprmprod  16708  coprmproddvdslem  16709  cncongr1  16714  cncongr2  16715  prm2orodd  16738  2mulprm  16740  nnnn0modprm0  16853  prm23lt5  16861  prm23ge5  16862  dvdsprmpweqnn  16932  dvdsprmpweqle  16933  oddprmdvds  16950  prmpwdvds  16951  prmreclem4  16966  ramcl  17076  prmgaplem6  17103  prmgaplem7  17104  prmgaplem8  17105  cshwshashlem1  17143  cshwshashlem2  17144  cshwshashlem3  17145  cshwrepswhash1  17150  setsn0fun  17220  setsstruct2  17221  imasleval  17601  mreiincl  17654  mreexexd  17706  inveq  17835  cicsym  17865  cictr  17866  initoid  18068  termoid  18069  initoeu2lem0  18080  initoeu2lem1  18081  initoeu2lem2  18082  initoeu2  18083  fthestrcsetc  18219  fthsetcestrc  18234  drsdirfi  18375  isnmgm  18682  mgmhmlin  18737  issubmgm2  18741  sgrpass  18763  insubm  18853  mgm2nsgrplem3  18955  dfgrp3lem  19078  cyccom  19243  symg2bas  19434  symgfix2  19458  symgextf1  19463  gsmsymgrfix  19470  pmtrprfv3  19496  psgnunilem4  19539  efgi2  19767  0ringnnzr  20551  rnghmsscmap  20652  rnghmsubcsetclem2  20654  rngcinv  20659  funcrngcsetc  20662  funcrngcsetcALT  20663  rhmsscmap  20681  rhmsubcsetclem2  20683  rhmsubcrngclem2  20689  ringcbasbas  20695  funcringcsetc  20696  rhmsubclem4  20710  rngqiprngimfo  21334  psgndiflemB  21641  psgndiflemA  21642  elfrlmbasn0  21806  lmictra  21888  mpfrcl  22132  gsummoncoe1  22333  mamufacex  22421  matecl  22452  dmatelnd  22523  dmatscmcl  22530  scmateALT  22539  scmatsgrp1  22549  scmatf1  22558  mavmulsolcl  22578  cramerimplem1  22710  cramerimplem2  22711  pmatcollpw3fi1  22815  mp2pm2mplem4  22836  pm2mpfo  22841  chmaidscmat  22875  fvmptnn04ifb  22878  chfacfscmul0  22885  chfacfpmmul0  22889  cayhamlem1  22893  cayhamlem3  22914  cayleyhamilton1  22919  fiinopn  22928  tgcl  22997  distop  23023  isclo2  23117  iscldtop  23124  ssnei2  23145  opnnei  23149  pnfnei  23249  mnfnei  23250  tgcnp  23282  cnpnei  23293  1stcelcls  23490  txcnpi  23637  cnmptcom  23707  fbfinnfr  23870  isfildlem  23886  snfil  23893  fbunfip  23898  fgcl  23907  elfm2  23977  fmco  23990  fbflim2  24006  cnpflf2  24029  flimfcls  24055  tmdgsum  24124  neibl  24535  tngngpim  24701  fgcfil  25324  caubl  25361  volsuplem  25609  ellimc3  25934  dvnadd  25985  dvnres  25987  cpnord  25991  dvnfre  26010  ply1divex  26196  cxpmul2  26749  fsumdvdsmul  27256  zabsle1  27358  gausslemma2dlem1a  27427  gausslemma2dlem3  27430  lgsquad2lem2  27447  2lgs  27469  2sq2  27495  2sqnn0  27500  2sqnn  27501  2sqreultlem  27509  2sqreunnltlem  27512  qabvexp  27688  sltval2  27719  nolt02o  27758  ssltun1  27871  scutun12  27873  madebday  27956  mulsprop  28174  precsexlem8  28256  precsexlem9  28257  noseqind  28316  om2noseqrdg  28328  peano5uzs  28408  axcontlem4  29000  umgredgprv  29142  umgrnloop  29143  upgrpredgv  29174  upgredgpr  29177  edglnl  29178  usgredgprvALT  29230  usgrnloopALT  29238  usgredg2v  29262  fusgrfis  29365  nbuhgr2vtx1edgblem  29386  nb3grprlem1  29415  cusgrsize2inds  29489  cusgrfi  29494  fusgrn0degnn0  29535  uspgrloopvtxel  29552  vtxdginducedm1lem4  29578  uhgr0edg0rgrb  29610  wlkl1loop  29674  wlk1walk  29675  upgriswlk  29677  upgrwlkvtxedg  29681  uspgr2wlkeq  29682  wlkv0  29687  wlksoneq1eq2  29700  wlkon2n0  29702  wlkreslem  29705  wlkres  29706  lfgrwlkprop  29723  pthdivtx  29765  2pthnloop  29767  spthonepeq  29788  uhgrwkspthlem2  29790  uhgrwkspth  29791  usgr2wlkneq  29792  usgr2trlncl  29796  usgr2pthlem  29799  usgr2pth  29800  cyclnspth  29836  lfgrn1cycl  29838  usgr2trlncrct  29839  uspgrn2crct  29841  crctcshwlkn0lem3  29845  crctcshwlkn0lem5  29847  wwlknp  29876  wspthneq1eq2  29893  0enwwlksnge1  29897  wlklnwwlkln1  29901  wlkiswwlks2  29908  wlkiswwlksupgr2  29910  wlklnwwlkln2lem  29915  wwlksnred  29925  wwlksnextbi  29927  wwlksnredwwlkn0  29929  wwlksnextwrd  29930  wwlksnextinj  29932  wwlksnextproplem3  29944  wwlksnextprop  29945  wspthsnwspthsnon  29949  wspthsnonn0vne  29950  2pthon3v  29976  umgr2adedgwlkonALT  29980  umgr2wlk  29982  umgr2wlkon  29983  umgrwwlks2on  29990  elwspths2on  29993  usgr2wspthons3  29997  elwwlks2  29999  rusgrnumwwlk  30008  clwwlkccatlem  30021  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  clwlkclwwlkf1lem3  30038  erclwwlkeqlen  30051  clwwlknwwlksn  30070  loopclwwlkn1b  30074  clwwlkf1  30081  wwlksext2clwwlk  30089  eleclclwwlknlem2  30093  umgr2cwwk2dif  30096  eleclclwwlkn  30108  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  clwwlknonwwlknonb  30138  clwwlknonex2lem2  30140  clwwlknonex2  30141  1pthon2v  30185  upgr3v3e3cycl  30212  uhgr3cyclexlem  30213  uhgr3cyclex  30214  eupth2lem3lem4  30263  frgr3vlem1  30305  frgr3vlem2  30306  3vfriswmgrlem  30309  3vfriswmgr  30310  3cyclfrgrrn1  30317  n4cyclfrgr  30323  frgrncvvdeqlem3  30333  frgrncvvdeqlem6  30336  frgrncvvdeqlem7  30337  frgrncvvdeqlem8  30338  frgrwopreglem4a  30342  frgrwopreglem3  30346  frgrwopreg1  30350  frgrwopreg2  30351  frgrwopreglem5lem  30352  frgrwopreglem5ALT  30354  frgrwopreg  30355  fusgr2wsp2nb  30366  2wspmdisj  30369  numclwwlk1lem2foa  30386  numclwwlk1lem2f1  30389  numclwwlk1lem2fo  30390  numclwwlk1  30393  wlkl0  30399  numclwwlk2lem1  30408  numclwlk2lem2f  30409  numclwlk2lem2f1o  30411  frgrreg  30426  frgrregord013  30427  frgrregord13  30428  friendshipgt3  30430  friendship  30431  eulplig  30517  ipassi  30873  ubthlem2  30903  isch3  31273  shintcli  31361  shmodsi  31421  spansncvi  31684  hoaddsub  31848  eigorthi  31869  pjss2coi  32196  pjnormssi  32200  pj3cor1i  32241  strb  32290  dmdmd  32332  mdsl0  32342  csmdsymi  32366  chrelat2i  32397  mdsymlem3  32437  mdsymlem6  32440  sumdmdlem2  32451  opreu2reuALT  32505  ssrelf  32637  spthcycl  35097  loop1cycl  35105  cvmlift2lem1  35270  satfrel  35335  satfrnmapom  35338  fmlafvel  35353  fmla1  35355  gonarlem  35362  gonar  35363  goalrlem  35364  goalr  35365  satffunlem  35369  satffunlem1lem1  35370  satffunlem2lem1  35372  satffun  35377  satefvfmla1  35393  mrsubvrs  35490  mclsax  35537  3ccased  35681  dfon2lem3  35749  rdgprc  35758  cgrextend  35972  btwndiff  35991  btwnconn1lem12  36062  brsegle  36072  broutsideof2  36086  funray  36104  in-ax8  36190  ss-ax8  36191  elicc3  36283  nn0prpwlem  36288  nn0prpw  36289  fnessref  36323  neibastop2lem  36326  filnetlem4  36347  meran1  36377  waj-ax  36380  arg-ax  36382  bj-nnclavc  36514  bj-con2com  36527  bj-axdd2  36558  bj-alrimg  36585  bj-exlimg  36589  bj-exalimi  36599  bj-cbvalimt  36605  bj-eximcom  36609  bj-ssbid1ALT  36631  bj-sb  36653  bj-snsetex  36929  bj-restpw  37058  bj-finsumval0  37251  mptsnunlem  37304  icoreclin  37323  relowlpssretop  37330  inunissunidif  37341  rdgssun  37344  finorwe  37348  domalom  37370  wl-dral1d  37485  wl-exeq  37488  wl-lem-exsb  37520  poimirlem29  37609  poimirlem32  37612  fdc  37705  seqpo  37707  incsequz  37708  isismty  37761  ismtybndlem  37766  heibor1lem  37769  ismgmOLD  37810  isexid2  37815  ghomco  37851  pridlc  38031  relcnveq3  38277  elrelscnveq3  38447  cdleme18d  40252  tendovalco  40722  cdlemn11pre  41167  dihord2pre  41182  indstrd  42150  unitscyglem3  42154  nnadddir  42259  eu6w  42631  incssnn0  42667  fphpd  42772  jm2.19lem3  42948  setindtr  42981  islssfg2  43028  mpaaeu  43107  ordnexbtwnsuc  43229  oaabsb  43256  succlg  43290  oacl2g  43292  omabs2  43294  omcl2  43295  omcl3g  43296  pr2cv  43510  refimssco  43569  iunrelexpmin1  43670  iunrelexpmin2  43674  trclimalb2  43688  clsk1indlem3  44005  tfindsd  44174  mnurndlem1  44250  nzss  44286  sb5ALT  44496  truniALT  44512  ee223  44605  3orbi123VD  44821  sbc3orgVD  44822  exbirVD  44824  exbiriVD  44825  sbcim2gVD  44846  trsbcVD  44848  truniALTVD  44849  onfrALTlem3VD  44858  onfrALTlem2VD  44860  csbrngVD  44867  19.41rgVD  44873  ax6e2eqVD  44878  ax6e2ndeqVD  44880  2uasbanhVD  44882  sb5ALTVD  44884  vk15.4jVD  44885  infxrunb3rnmpt  45343  stoweidlem26  45947  et-equeucl  46793  hirstL-ax3  46807  rexsb  47014  rexrsb  47015  euoreqb  47024  2reu8i  47028  afvres  47087  tz6.12-afv  47088  afvco2  47091  afv2orxorb  47143  afv2res  47154  tz6.12-afv2  47155  tz6.12i-afv2  47158  dfatcolem  47170  zm1nn  47217  2ffzoeq  47242  smonoord  47245  iccpartiltu  47296  iccpartlt  47298  iccpartltu  47299  iccpartgtl  47300  iccpartgt  47301  iccpartleu  47302  iccpartgel  47303  icceuelpart  47310  iccpartnel  47312  lswn0  47318  ichnreuop  47346  ichreuopeq  47347  prsprel  47361  sprsymrelfvlem  47364  sprsymrelf1lem  47365  sprsymrelfolem2  47367  prproropf1olem4  47380  paireqne  47385  prprelb  47390  reupr  47396  goldbachth  47421  odz2prm2pw  47437  fmtno4prmfac  47446  fmtno4prmfac193  47447  prmdvdsfmtnof1lem2  47459  2pwp1prmfmtno  47464  lighneallem2  47480  lighneallem4b  47483  lighneallem4  47484  requad2  47497  odd2prm2  47592  mogoldbblem  47594  gbepos  47632  gbowgt5  47636  gbowge7  47637  stgoldbwt  47650  sbgoldbwt  47651  sbgoldbst  47652  sbgoldbaltlem1  47653  sbgoldbalt  47655  sbgoldbo  47661  nnsum3primesle9  47668  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  bgoldbtbndlem1  47679  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbnd  47683  dfnbgr6  47729  isuspgrimlem  47758  uhgrimisgrgric  47783  clnbgrgrim  47786  usgrgrtrirex  47799  grilcbri2  47828  grlicsym  47830  grlictr  47832  gricgrlic  47835  upgrwlkupwlk  47863  uspgrsprf1  47870  lmod0rng  47952  lidldomn1  47954  rngccatidALTV  47995  rngcinvALTV  47999  rhmsubcALTVlem4  48007  funcringcsetcALTV2lem9  48021  ringccatidALTV  48029  ringcbasbasALTV  48035  ztprmneprm  48072  pgrpgt2nabl  48091  lmodvsmdi  48107  ply1mulgsumlem2  48116  lincsumcl  48160  ellcoellss  48164  linindslinci  48177  islinindfis  48178  lincext3  48185  lindslinindimp2lem4  48190  lindslinindsimp2lem5  48191  lindslinindsimp2  48192  lindsrng01  48197  ldepspr  48202  lincresunit3lem1  48208  elfzolborelfzop1  48248  dignn0ldlem  48336  nn0sumshdiglem1  48355  1arymaptf1  48376  2arymaptf1  48387  rrx2xpref1o  48452  rrx2plord2  48456  rrx2plordisom  48457  line2ylem  48485  line2xlem  48487  line2y  48489  itschlc0xyqsol1  48500  inlinecirc02plem  48520  fullthinc  48713  tfis2d  48772  onsetrec  48800