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  2358  cbv1  2401  ax12b  2423  axc11n  2425  dvelimdf  2448  equvel  2455  dfsb1  2480  sbied  2502  dfmoeu  2530  mo3  2558  mo4  2560  2mo  2642  2eu6  2651  exists2  2656  pm2.61dne  3012  rexlimdv  3133  r19.21v  3159  r19.12  3290  2gencl  3493  3gencl  3494  vtocl2ga  3547  vtocl2gaf  3548  vtocl3gaf  3550  vtocl3ga  3552  vtocl4ga  3555  rspccv  3588  ceqex  3621  mob  3691  euind  3698  reuind  3727  2reu1  3863  sseq2  3976  nelss  4015  rexdifi  4116  reupick2  4297  disjeq0  4422  uneqdifeq  4459  sspw  4577  ssprsseq  4792  preq12b  4817  prnebg  4823  prel12g  4831  3elpr2eq  4873  iinss2  5024  trintss  5236  dtruALT2  5328  reusv2lem1  5356  alxfr  5365  ralxfrALT  5373  exexneq  5397  dtruOLD  5404  copsexgw  5453  copsexg  5454  snopeqop  5469  propeqop  5470  opthhausdorff  5480  opthhausdorff0  5481  pofun  5567  solin  5576  frss  5605  2optocl  5737  3optocl  5738  ssrel  5748  ssrelOLD  5749  ssrel2  5751  ssrelrel  5762  relop  5817  dfres3  5958  asymref2  6093  xpidtr  6098  trin2  6099  poltletr  6108  imadifssran  6127  xp11  6151  relcnvtrg  6242  reuop  6269  tz7.7  6361  ordtr2  6380  suc11  6444  iotavalOLD  6488  funmoOLD  6535  fundif  6568  fss  6707  f0dom0  6747  fv3  6879  tz6.12i  6889  mpteqb  6990  fveqdmss  7053  eldmrexrnb  7067  funopsn  7123  funsndifnop  7126  tpres  7178  funfvima  7207  fvclss  7218  f1veqaeq  7234  fvf1pr  7285  isoselem  7319  oprabv  7452  ovg  7557  elovmpt3rab1  7652  sorpsscmpl  7713  iunpw  7750  trom  7854  limom  7861  peano5  7872  focdmex  7937  funelss  8029  funeldmdif  8030  bropopvvv  8072  bropfvvvvlem  8073  f1o2ndf1  8104  poxp  8110  soxp  8111  poxp2  8125  frxp2  8126  frxp3  8133  suppimacnv  8156  ressuppss  8165  ressuppssdif  8167  tposfn2  8230  wfr3g  8301  onnseq  8316  smoel  8332  smogt  8339  smoiso2  8341  tfr3  8370  tz7.48-2  8413  tz7.48-3  8415  tz7.49  8416  oecl  8504  oaordex  8525  oalimcl  8527  oaass  8528  omordi  8533  omlimcl  8545  odi  8546  omeulem1  8549  oen0  8553  nnawordi  8588  nnaass  8589  nnmordi  8598  omabs  8618  omsmolem  8624  naddssim  8652  brinxper  8703  iiner  8765  2ecoptocl  8784  3ecoptocl  8785  undifixp  8910  xpdom2  9041  xpf1o  9109  infensuc  9125  findcard2  9134  php  9177  isinf  9214  isinfOLD  9215  unblem2  9247  fodomfir  9286  infssuni  9304  finsschain  9317  fsuppunfi  9346  fsuppunbi  9347  marypha1  9392  hartogs  9504  card2on  9514  card2inf  9515  xpwdomg  9545  elirrv  9556  en3lp  9574  preleqg  9575  inf3lem1  9588  inf3lem2  9589  inf3lem3  9590  inf3lem5  9592  noinfep  9620  ttrclss  9680  ttrclselem2  9686  trcl  9688  tcel  9705  frr3g  9716  rankonidlem  9788  scottex  9845  djuunxp  9881  eldju2ndl  9884  updjud  9894  dif1card  9970  fodomnum  10017  cardaleph  10049  kmlem9  10119  kmlem13  10123  cflim2  10223  cfsmolem  10230  infpssrlem3  10265  isfin7-2  10356  fin1a2lem6  10365  fin1a2lem12  10371  domtriomlem  10402  axdc3lem4  10413  axdc4lem  10415  zorn2lem3  10458  zorn2lem4  10459  zorn2lem5  10460  zorn2lem7  10462  zornn0g  10465  axdclem2  10480  ondomon  10523  alephval2  10532  cfpwsdom  10544  wuncval2  10707  grupr  10757  gruiun  10759  ingru  10775  grothomex  10789  indpi  10867  nqereu  10889  prlem934  10993  reclem2pr  11008  mulgt0sr  11065  supsrlem  11071  1re  11181  dedekind  11344  lemul1a  12043  squeeze0  12093  peano5nni  12196  nnunb  12445  nn0lt2  12604  nn0le2is012  12605  fzind  12639  nn0ind-raph  12641  zindd  12642  eluzaddOLD  12835  uzin  12840  nn01to3  12907  xnn0xadd0  13214  xmulasslem  13252  icoshft  13441  fzen  13509  uzsubsubfz  13514  elfz0ubfz0  13600  elfz0fzfz0  13601  fz0fzelfz0  13602  elfzmlbp  13607  elfzodifsumelfzo  13699  ssfzo12bi  13729  fzoopth  13730  elfzonelfzo  13737  elfznelfzo  13740  injresinjlem  13755  injresinj  13756  modfzo0difsn  13915  modsumfzodifsn  13916  addmodlteq  13918  ssnn0fi  13957  fsuppmapnn0fiub0  13965  expcllem  14044  expeq0  14064  mulexp  14073  leexp2r  14146  bernneq  14201  facdiv  14259  hasheqf1oi  14323  hashnn0n0nn  14363  hashss  14381  hashgt12el  14394  hashgt12el2  14395  hashimarni  14413  hashle2pr  14449  pr2pwpr  14451  hashge2el2dif  14452  hashge2el2difr  14453  hashtpg  14457  hashge3el3dif  14459  exprelprel  14462  hash1to3  14464  hash3tpde  14465  tpfo  14472  fundmge2nop0  14474  fi1uzind  14479  ccatsymb  14554  swrdnd  14626  swrdnd2  14627  swrdnnn0nd  14628  swrdnd0  14629  pfxnd0  14660  swrdswrdlem  14676  swrdswrd  14677  pfxccatin12lem2a  14699  pfxccatin12lem1  14700  swrdccatin2  14701  pfxccatin12lem2  14703  pfxccatin12lem3  14704  pfxccat3  14706  swrdccat  14707  swrdccat3blem  14711  repsdf2  14750  repswswrd  14756  cshwidxmod  14775  cshwidx0  14778  cshf1  14782  cshweqrep  14793  cshw1  14794  cshwsexaOLD  14797  2cshwcshw  14798  scshwfzeqfzo  14799  cshwcsh2id  14801  wwlktovfo  14931  relexpaddg  15026  iseraltlem2  15656  modfsummods  15766  clim2prod  15861  prodfn0  15867  prodfrec  15868  prodmo  15909  fprodabs  15947  binomfallfac  16014  fprodefsum  16068  dvdsaddre2b  16284  addmodlteqALT  16302  oddge22np1  16326  nn0enne  16354  nn0o1gt2  16358  sumeven  16364  sumodd  16365  dvdslegcd  16481  gcdneg  16499  dfgcd2  16523  rplpwr  16535  lcmf  16610  lcmftp  16613  lcmfunsnlem2lem1  16615  lcmfunsnlem2  16617  lcmfdvdsb  16620  coprmdvds1  16629  qredeq  16634  coprmprod  16638  coprmproddvdslem  16639  cncongr1  16644  cncongr2  16645  prm2orodd  16668  2mulprm  16670  nnnn0modprm0  16784  prm23lt5  16792  prm23ge5  16793  dvdsprmpweqnn  16863  dvdsprmpweqle  16864  oddprmdvds  16881  prmpwdvds  16882  prmreclem4  16897  ramcl  17007  prmgaplem6  17034  prmgaplem7  17035  prmgaplem8  17036  cshwshashlem1  17073  cshwshashlem2  17074  cshwshashlem3  17075  cshwrepswhash1  17080  setsn0fun  17150  setsstruct2  17151  imasleval  17511  mreiincl  17564  mreexexd  17616  inveq  17743  cicsym  17773  cictr  17774  initoid  17970  termoid  17971  initoeu2lem0  17982  initoeu2lem1  17983  initoeu2lem2  17984  initoeu2  17985  fthestrcsetc  18118  fthsetcestrc  18133  drsdirfi  18273  isnmgm  18578  mgmhmlin  18633  issubmgm2  18637  sgrpass  18659  insubm  18752  mgm2nsgrplem3  18854  dfgrp3lem  18977  cyccom  19142  symg2bas  19330  symgfix2  19353  symgextf1  19358  gsmsymgrfix  19365  pmtrprfv3  19391  psgnunilem4  19434  efgi2  19662  0ringnnzr  20441  rnghmsscmap  20546  rnghmsubcsetclem2  20548  rngcinv  20553  funcrngcsetc  20556  funcrngcsetcALT  20557  rhmsscmap  20575  rhmsubcsetclem2  20577  rhmsubcrngclem2  20583  ringcbasbas  20589  funcringcsetc  20590  rhmsubclem4  20604  rngqiprngimfo  21218  psgndiflemB  21516  psgndiflemA  21517  elfrlmbasn0  21679  lmictra  21761  mpfrcl  21999  gsummoncoe1  22202  mamufacex  22290  matecl  22319  dmatelnd  22390  dmatscmcl  22397  scmateALT  22406  scmatsgrp1  22416  scmatf1  22425  mavmulsolcl  22445  cramerimplem1  22577  cramerimplem2  22578  pmatcollpw3fi1  22682  mp2pm2mplem4  22703  pm2mpfo  22708  chmaidscmat  22742  fvmptnn04ifb  22745  chfacfscmul0  22752  chfacfpmmul0  22756  cayhamlem1  22760  cayhamlem3  22781  cayleyhamilton1  22786  fiinopn  22795  tgcl  22863  distop  22889  isclo2  22982  iscldtop  22989  ssnei2  23010  opnnei  23014  pnfnei  23114  mnfnei  23115  tgcnp  23147  cnpnei  23158  1stcelcls  23355  txcnpi  23502  cnmptcom  23572  fbfinnfr  23735  isfildlem  23751  snfil  23758  fbunfip  23763  fgcl  23772  elfm2  23842  fmco  23855  fbflim2  23871  cnpflf2  23894  flimfcls  23920  tmdgsum  23989  neibl  24396  tngngpim  24554  fgcfil  25178  caubl  25215  volsuplem  25463  ellimc3  25787  dvnadd  25838  dvnres  25840  cpnord  25844  dvnfre  25863  ply1divex  26049  cxpmul2  26605  fsumdvdsmul  27112  zabsle1  27214  gausslemma2dlem1a  27283  gausslemma2dlem3  27286  lgsquad2lem2  27303  2lgs  27325  2sq2  27351  2sqnn0  27356  2sqnn  27357  2sqreultlem  27365  2sqreunnltlem  27368  qabvexp  27544  sltval2  27575  nolt02o  27614  ssltun1  27727  scutun12  27729  madebday  27818  mulsprop  28040  precsexlem8  28123  precsexlem9  28124  noseqind  28193  om2noseqrdg  28205  n0cutlt  28256  peano5uzs  28299  expadds  28327  axcontlem4  28901  umgredgprv  29041  umgrnloop  29042  upgrpredgv  29073  upgredgpr  29076  edglnl  29077  usgredgprvALT  29129  usgrnloopALT  29137  usgredg2v  29161  fusgrfis  29264  nbuhgr2vtx1edgblem  29285  nb3grprlem1  29314  cusgrsize2inds  29388  cusgrfi  29393  fusgrn0degnn0  29434  uspgrloopvtxel  29451  vtxdginducedm1lem4  29477  uhgr0edg0rgrb  29509  wlkl1loop  29573  wlk1walk  29574  upgriswlk  29576  upgrwlkvtxedg  29580  uspgr2wlkeq  29581  wlkv0  29586  wlksoneq1eq2  29599  wlkon2n0  29601  wlkreslem  29604  wlkres  29605  lfgrwlkprop  29622  pthdivtx  29664  2pthnloop  29668  spthonepeq  29689  uhgrwkspthlem2  29691  uhgrwkspth  29692  usgr2wlkneq  29693  usgr2trlncl  29697  usgr2pthlem  29700  usgr2pth  29701  cyclnspth  29738  lfgrn1cycl  29742  usgr2trlncrct  29743  uspgrn2crct  29745  crctcshwlkn0lem3  29749  crctcshwlkn0lem5  29751  wwlknp  29780  wspthneq1eq2  29797  0enwwlksnge1  29801  wlklnwwlkln1  29805  wlkiswwlks2  29812  wlkiswwlksupgr2  29814  wlklnwwlkln2lem  29819  wwlksnred  29829  wwlksnextbi  29831  wwlksnredwwlkn0  29833  wwlksnextwrd  29834  wwlksnextinj  29836  wwlksnextproplem3  29848  wwlksnextprop  29849  wspthsnwspthsnon  29853  wspthsnonn0vne  29854  2pthon3v  29880  umgr2adedgwlkonALT  29884  umgr2wlk  29886  umgr2wlkon  29887  umgrwwlks2on  29894  elwspths2on  29897  usgr2wspthons3  29901  elwwlks2  29903  rusgrnumwwlk  29912  clwwlkccatlem  29925  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  clwlkclwwlkf1lem3  29942  erclwwlkeqlen  29955  clwwlknwwlksn  29974  loopclwwlkn1b  29978  clwwlkf1  29985  wwlksext2clwwlk  29993  eleclclwwlknlem2  29997  umgr2cwwk2dif  30000  eleclclwwlkn  30012  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  clwwlknonwwlknonb  30042  clwwlknonex2lem2  30044  clwwlknonex2  30045  1pthon2v  30089  upgr3v3e3cycl  30116  uhgr3cyclexlem  30117  uhgr3cyclex  30118  eupth2lem3lem4  30167  frgr3vlem1  30209  frgr3vlem2  30210  3vfriswmgrlem  30213  3vfriswmgr  30214  3cyclfrgrrn1  30221  n4cyclfrgr  30227  frgrncvvdeqlem3  30237  frgrncvvdeqlem6  30240  frgrncvvdeqlem7  30241  frgrncvvdeqlem8  30242  frgrwopreglem4a  30246  frgrwopreglem3  30250  frgrwopreg1  30254  frgrwopreg2  30255  frgrwopreglem5lem  30256  frgrwopreglem5ALT  30258  frgrwopreg  30259  fusgr2wsp2nb  30270  2wspmdisj  30273  numclwwlk1lem2foa  30290  numclwwlk1lem2f1  30293  numclwwlk1lem2fo  30294  numclwwlk1  30297  wlkl0  30303  numclwwlk2lem1  30312  numclwlk2lem2f  30313  numclwlk2lem2f1o  30315  frgrreg  30330  frgrregord013  30331  frgrregord13  30332  friendshipgt3  30334  friendship  30335  eulplig  30421  ipassi  30777  ubthlem2  30807  isch3  31177  shintcli  31265  shmodsi  31325  spansncvi  31588  hoaddsub  31752  eigorthi  31773  pjss2coi  32100  pjnormssi  32104  pj3cor1i  32145  strb  32194  dmdmd  32236  mdsl0  32246  csmdsymi  32270  chrelat2i  32301  mdsymlem3  32341  mdsymlem6  32344  sumdmdlem2  32355  opreu2reuALT  32413  ssrelf  32550  gsumwun  33012  onvf1odlem4  35100  spthcycl  35123  loop1cycl  35131  cvmlift2lem1  35296  satfrel  35361  satfrnmapom  35364  fmlafvel  35379  fmla1  35381  gonarlem  35388  gonar  35389  goalrlem  35390  goalr  35391  satffunlem  35395  satffunlem1lem1  35396  satffunlem2lem1  35398  satffun  35403  satefvfmla1  35419  mrsubvrs  35516  mclsax  35563  3ccased  35713  dfon2lem3  35780  rdgprc  35789  cgrextend  36003  btwndiff  36022  btwnconn1lem12  36093  brsegle  36103  broutsideof2  36117  funray  36135  in-ax8  36219  ss-ax8  36220  elicc3  36312  nn0prpwlem  36317  nn0prpw  36318  fnessref  36352  neibastop2lem  36355  filnetlem4  36376  meran1  36406  waj-ax  36409  arg-ax  36411  bj-nnclavc  36543  bj-con2com  36556  bj-axdd2  36587  bj-alrimg  36614  bj-exlimg  36618  bj-exalimi  36628  bj-cbvalimt  36634  bj-eximcom  36638  bj-ssbid1ALT  36660  bj-sb  36682  bj-snsetex  36958  bj-restpw  37087  bj-finsumval0  37280  mptsnunlem  37333  icoreclin  37352  relowlpssretop  37359  inunissunidif  37370  rdgssun  37373  finorwe  37377  domalom  37399  wl-dral1d  37526  wl-exeq  37529  wl-lem-exsb  37561  poimirlem29  37650  poimirlem32  37653  fdc  37746  seqpo  37748  incsequz  37749  isismty  37802  ismtybndlem  37807  heibor1lem  37810  ismgmOLD  37851  isexid2  37856  ghomco  37892  pridlc  38072  relcnveq3  38316  elrelscnveq3  38489  cdleme18d  40296  tendovalco  40766  cdlemn11pre  41211  dihord2pre  41226  indstrd  42188  unitscyglem3  42192  nnadddir  42265  eu6w  42671  incssnn0  42706  fphpd  42811  jm2.19lem3  42987  setindtr  43020  islssfg2  43067  mpaaeu  43146  ordnexbtwnsuc  43263  oaabsb  43290  succlg  43324  oacl2g  43326  omabs2  43328  omcl2  43329  omcl3g  43330  pr2cv  43544  refimssco  43603  iunrelexpmin1  43704  iunrelexpmin2  43708  trclimalb2  43722  clsk1indlem3  44039  tfindsd  44206  mnurndlem1  44277  nzss  44313  sb5ALT  44522  truniALT  44538  ee223  44631  3orbi123VD  44846  sbc3orgVD  44847  exbirVD  44849  exbiriVD  44850  sbcim2gVD  44871  trsbcVD  44873  truniALTVD  44874  onfrALTlem3VD  44883  onfrALTlem2VD  44885  csbrngVD  44892  19.41rgVD  44898  ax6e2eqVD  44903  ax6e2ndeqVD  44905  2uasbanhVD  44907  sb5ALTVD  44909  vk15.4jVD  44910  infxrunb3rnmpt  45431  stoweidlem26  46031  et-equeucl  46877  hirstL-ax3  46897  rexsb  47104  rexrsb  47105  euoreqb  47114  2reu8i  47118  afvres  47177  tz6.12-afv  47178  afvco2  47181  afv2orxorb  47233  afv2res  47244  tz6.12-afv2  47245  tz6.12i-afv2  47248  dfatcolem  47260  zm1nn  47307  2ffzoeq  47332  smonoord  47376  iccpartiltu  47427  iccpartlt  47429  iccpartltu  47430  iccpartgtl  47431  iccpartgt  47432  iccpartleu  47433  iccpartgel  47434  icceuelpart  47441  iccpartnel  47443  lswn0  47449  ichnreuop  47477  ichreuopeq  47478  prsprel  47492  sprsymrelfvlem  47495  sprsymrelf1lem  47496  sprsymrelfolem2  47498  prproropf1olem4  47511  paireqne  47516  prprelb  47521  reupr  47527  goldbachth  47552  odz2prm2pw  47568  fmtno4prmfac  47577  fmtno4prmfac193  47578  prmdvdsfmtnof1lem2  47590  2pwp1prmfmtno  47595  lighneallem2  47611  lighneallem4b  47614  lighneallem4  47615  requad2  47628  odd2prm2  47723  mogoldbblem  47725  gbepos  47763  gbowgt5  47767  gbowge7  47768  stgoldbwt  47781  sbgoldbwt  47782  sbgoldbst  47783  sbgoldbaltlem1  47784  sbgoldbalt  47786  sbgoldbo  47792  nnsum3primesle9  47799  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  bgoldbtbndlem1  47810  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  bgoldbtbnd  47814  dfnbgr6  47861  isuspgrimlem  47899  uhgrimisgrgric  47935  clnbgrgrim  47938  usgrgrtrirex  47953  isubgr3stgrlem4  47972  grilcbri2  48007  grlicsym  48009  grlictr  48011  gricgrlic  48014  gpgvtxedg0  48058  gpgvtxedg1  48059  gpgedg2ov  48061  gpgedg2iv  48062  pgnioedg1  48102  pgnioedg2  48103  pgnioedg3  48104  pgnioedg4  48105  pgnioedg5  48106  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem5lem1  48114  pgnbgreunbgrlem5lem2  48115  pgnbgreunbgrlem5lem3  48116  pgnbgreunbgrlem6  48118  upgrwlkupwlk  48132  uspgrsprf1  48139  lmod0rng  48221  lidldomn1  48223  rngccatidALTV  48264  rngcinvALTV  48268  rhmsubcALTVlem4  48276  funcringcsetcALTV2lem9  48290  ringccatidALTV  48298  ringcbasbasALTV  48304  ztprmneprm  48339  pgrpgt2nabl  48358  lmodvsmdi  48371  ply1mulgsumlem2  48380  lincsumcl  48424  ellcoellss  48428  linindslinci  48441  islinindfis  48442  lincext3  48449  lindslinindimp2lem4  48454  lindslinindsimp2lem5  48455  lindslinindsimp2  48456  lindsrng01  48461  ldepspr  48466  lincresunit3lem1  48472  elfzolborelfzop1  48512  dignn0ldlem  48595  nn0sumshdiglem1  48614  1arymaptf1  48635  2arymaptf1  48646  rrx2xpref1o  48711  rrx2plord2  48715  rrx2plordisom  48716  line2ylem  48744  line2xlem  48746  line2y  48748  itschlc0xyqsol1  48759  inlinecirc02plem  48779  fullthinc  49443  tfis2d  49673  onsetrec  49701