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  158  expt  179  jad  189  pm2.61  194  syl5ibcom  247  syl5ibrcom  249  pm5.501  369  impcom  410  impd  413  expcom  416  expdcom  417  simplbi2com  505  imdistanri  572  jaod  855  orel1  885  pm2.62  896  pm2.75  930  pm2.64  938  ccased  1033  dedlem0b  1039  3impd  1344  3expd  1349  mp3an1i  1450  norassOLD  1534  minimp  1622  meredith  1642  19.35  1878  speimfw  1966  equtrr  2029  equeucl  2031  sb56OLD  2278  sbiedw  2332  sbiedwOLD  2333  cbv1v  2356  exsb  2378  cbv1  2422  ax12b  2446  axc11n  2448  dvelimdf  2471  equvel  2479  dfsb1  2510  sbequ2OLDOLD  2514  sbied  2545  sbequ2ALT  2580  sbiedALT  2614  dfmoeu  2618  mo3  2648  mo4  2650  2mo  2733  2eu6  2742  exists2  2747  rexlimdv  3283  r19.12  3324  r19.12OLD  3327  r19.35  3341  2gencl  3535  3gencl  3536  vtocl2ga  3575  rspccv  3620  ceqex  3645  mob  3708  euind  3715  reuind  3744  2reu1  3881  sseq2  3993  nelss  4030  rexdifi  4122  reupick2  4289  rspn0  4313  disjeq0  4405  uneqdifeq  4438  sspw  4552  ssprsseq  4758  preq12b  4781  prnebg  4786  prel12g  4794  3elpr2eq  4837  iinss2  4981  trintss  5189  dtru  5271  reusv2lem1  5299  alxfr  5308  ralxfrALT  5316  copsexgw  5381  copsexg  5382  snopeqop  5396  propeqop  5397  opthhausdorff  5407  opthhausdorff0  5408  pocl  5481  pofun  5491  solin  5498  frss  5522  2optocl  5646  3optocl  5647  ssrel  5657  ssrel2  5659  ssrelrel  5669  relop  5721  dfres3  5858  asymref2  5977  xpidtr  5982  trin2  5983  poltletr  5992  xp11  6032  relcnvtrg  6119  reuop  6144  tz7.7  6217  ordtr2  6235  suc11  6294  iotaval  6329  funmo  6371  fundif  6403  fss  6527  f0dom0  6563  fv3  6688  tz6.12i  6696  mpteqb  6787  fveqdmss  6846  eldmrexrnb  6858  funopsn  6910  funsndifnop  6913  tpres  6963  funfvima  6992  fvclss  7001  f1veqaeq  7015  isoselem  7094  oprabv  7214  ovg  7313  elovmpt3rab1  7405  sorpsscmpl  7460  iunpw  7493  ordom  7589  limom  7595  peano5  7605  fornex  7657  funelss  7746  funeldmdif  7747  bropopvvv  7785  bropfvvvvlem  7786  f1o2ndf1  7818  poxp  7822  soxp  7823  suppimacnv  7841  ressuppss  7849  ressuppssdif  7851  tposfn2  7914  wfr3g  7953  onnseq  7981  smoel  7997  smogt  8004  smoiso2  8006  tfr3  8035  tz7.48-2  8078  tz7.48-3  8080  tz7.49  8081  oecl  8162  oaordex  8184  oalimcl  8186  oaass  8187  omordi  8192  omlimcl  8204  odi  8205  omeulem1  8208  oen0  8212  nnawordi  8247  nnaass  8248  nnmordi  8257  omabs  8274  omsmolem  8280  iiner  8369  2ecoptocl  8388  3ecoptocl  8389  undifixp  8498  xpdom2  8612  xpf1o  8679  infensuc  8695  php  8701  onomeneq  8708  isinf  8731  findcard2  8758  unblem2  8771  infssuni  8815  finsschain  8831  fsuppunfi  8853  fsuppunbi  8854  marypha1  8898  hartogs  9008  card2on  9018  card2inf  9019  xpwdomg  9049  elirrv  9060  en3lp  9077  preleqg  9078  inf3lem1  9091  inf3lem2  9092  inf3lem3  9093  inf3lem5  9095  noinfep  9123  trcl  9170  tcel  9187  rankonidlem  9257  scottex  9314  djuunxp  9350  eldju2ndl  9353  updjud  9363  dif1card  9436  fodomnum  9483  cardaleph  9515  kmlem9  9584  kmlem13  9588  cflim2  9685  cfsmolem  9692  infpssrlem3  9727  isfin7-2  9818  fin1a2lem6  9827  fin1a2lem12  9833  domtriomlem  9864  axdc3lem4  9875  axdc4lem  9877  zorn2lem3  9920  zorn2lem4  9921  zorn2lem5  9922  zorn2lem7  9924  zornn0g  9927  axdclem2  9942  ondomon  9985  alephval2  9994  cfpwsdom  10006  wuncval2  10169  grupr  10219  gruiun  10221  ingru  10237  grothomex  10251  indpi  10329  nqereu  10351  prlem934  10455  reclem2pr  10470  mulgt0sr  10527  supsrlem  10533  dedekind  10803  lemul1a  11494  squeeze0  11543  peano5nni  11641  nnunb  11894  nn0lt2  12046  nn0le2is012  12047  fzind  12081  nn0ind-raph  12083  zindd  12084  eluzadd  12274  uzin  12279  nn01to3  12342  xnn0xadd0  12641  xmulasslem  12679  icoshft  12860  fzen  12925  uzsubsubfz  12930  elfz0ubfz0  13012  elfz0fzfz0  13013  fz0fzelfz0  13014  elfzmlbp  13019  elfzodifsumelfzo  13104  ssfzo12bi  13133  elfzonelfzo  13140  elfznelfzo  13143  injresinjlem  13158  injresinj  13159  modfzo0difsn  13312  modsumfzodifsn  13313  addmodlteq  13315  ssnn0fi  13354  fsuppmapnn0fiub0  13362  expcllem  13441  expeq0  13460  mulexp  13469  leexp2r  13539  bernneq  13591  facdiv  13648  hasheqf1oi  13713  hashnn0n0nn  13753  hashss  13771  hashgt12el  13784  hashgt12el2  13785  hashimarni  13803  hashle2pr  13836  pr2pwpr  13838  hashge2el2dif  13839  hashge2el2difr  13840  hashtpg  13844  hashge3el3dif  13845  exprelprel  13848  hash1to3  13850  fundmge2nop0  13851  fi1uzind  13856  ccatsymb  13936  swrdnd  14016  swrdnd2  14017  swrdnnn0nd  14018  swrdnd0  14019  pfxnd0  14050  swrdswrdlem  14066  swrdswrd  14067  pfxccatin12lem2a  14089  pfxccatin12lem1  14090  swrdccatin2  14091  pfxccatin12lem2  14093  pfxccatin12lem3  14094  pfxccat3  14096  swrdccat  14097  swrdccat3blem  14101  repsdf2  14140  repswswrd  14146  cshwidxmod  14165  cshwidx0  14168  cshf1  14172  cshweqrep  14183  cshw1  14184  cshwsexa  14186  2cshwcshw  14187  scshwfzeqfzo  14188  cshwcsh2id  14190  wwlktovfo  14322  relexpaddg  14412  iseraltlem2  15039  modfsummods  15148  clim2prod  15244  prodfn0  15250  prodfrec  15251  prodmo  15290  fprodabs  15328  binomfallfac  15395  fprodefsum  15448  dvdsaddre2b  15657  addmodlteqALT  15675  oddge22np1  15698  nn0enne  15728  nn0o1gt2  15732  sumeven  15738  sumodd  15739  dvdslegcd  15853  gcdneg  15870  dfgcd2  15894  rplpwr  15907  lcmf  15977  lcmftp  15980  lcmfunsnlem2lem1  15982  lcmfunsnlem2  15984  lcmfdvdsb  15987  coprmdvds1  15996  qredeq  16001  coprmprod  16005  coprmproddvdslem  16006  cncongr1  16011  cncongr2  16012  prm2orodd  16035  2mulprm  16037  nnnn0modprm0  16143  prm23lt5  16151  prm23ge5  16152  dvdsprmpweqnn  16221  dvdsprmpweqle  16222  oddprmdvds  16239  prmpwdvds  16240  prmreclem4  16255  ramcl  16365  prmgaplem6  16392  prmgaplem7  16393  prmgaplem8  16394  cshwshashlem1  16429  cshwshashlem2  16430  cshwshashlem3  16431  cshwrepswhash1  16436  setsn0fun  16520  setsstruct2  16521  imasleval  16814  mreiincl  16867  mreexexd  16919  inveq  17044  cicsym  17074  cictr  17075  initoid  17265  termoid  17266  initoeu2lem0  17273  initoeu2lem1  17274  initoeu2lem2  17275  initoeu2  17276  fthestrcsetc  17400  fthsetcestrc  17415  drsdirfi  17548  isnmgm  17856  sgrpass  17907  insubm  17983  mgm2nsgrplem3  18085  dfgrp3lem  18197  cyccom  18346  symg2bas  18521  symgfix2  18544  symgextf1  18549  gsmsymgrfix  18556  pmtrprfv3  18582  psgnunilem4  18625  efgi2  18851  0ringnnzr  20042  mpfrcl  20298  gsummoncoe1  20472  psgndiflemB  20744  psgndiflemA  20745  elfrlmbasn0  20907  lmictra  20989  mamufacex  21000  matecl  21034  dmatelnd  21105  dmatscmcl  21112  scmateALT  21121  scmatsgrp1  21131  scmatf1  21140  mavmulsolcl  21160  cramerimplem1  21292  cramerimplem2  21293  pmatcollpw3fi1  21396  mp2pm2mplem4  21417  pm2mpfo  21422  chmaidscmat  21456  fvmptnn04ifb  21459  chfacfscmul0  21466  chfacfpmmul0  21470  cayhamlem1  21474  cayhamlem3  21495  cayleyhamilton1  21500  fiinopn  21509  tgcl  21577  distop  21603  isclo2  21696  iscldtop  21703  ssnei2  21724  opnnei  21728  pnfnei  21828  mnfnei  21829  tgcnp  21861  cnpnei  21872  1stcelcls  22069  txcnpi  22216  cnmptcom  22286  fbfinnfr  22449  isfildlem  22465  snfil  22472  fbunfip  22477  fgcl  22486  elfm2  22556  fmco  22569  fbflim2  22585  cnpflf2  22608  flimfcls  22634  tmdgsum  22703  neibl  23111  tngngpim  23268  fgcfil  23874  caubl  23911  volsuplem  24156  ellimc3  24477  dvnadd  24526  dvnres  24528  cpnord  24532  dvnfre  24549  ply1divex  24730  cxpmul2  25272  zabsle1  25872  gausslemma2dlem1a  25941  gausslemma2dlem3  25944  lgsquad2lem2  25961  2lgs  25983  2sq2  26009  2sqnn0  26014  2sqnn  26015  2sqreultlem  26023  2sqreunnltlem  26026  qabvexp  26202  axcontlem4  26753  umgredgprv  26892  umgrnloop  26893  upgrpredgv  26924  upgredgpr  26927  edglnl  26928  usgredgprvALT  26977  usgrnloopALT  26985  usgredg2v  27009  fusgrfis  27112  nbuhgr2vtx1edgblem  27133  nb3grprlem1  27162  cusgrsize2inds  27235  cusgrfi  27240  fusgrn0degnn0  27281  uspgrloopvtxel  27298  vtxdginducedm1lem4  27324  uhgr0edg0rgrb  27356  wlkl1loop  27419  wlk1walk  27420  upgriswlk  27422  upgrwlkvtxedg  27426  uspgr2wlkeq  27427  wlkv0  27432  wlklenvclwlkOLD  27437  wlksoneq1eq2  27446  wlkon2n0  27448  wlkreslem  27451  wlkres  27452  lfgrwlkprop  27469  pthdivtx  27510  2pthnloop  27512  spthonepeq  27533  uhgrwkspthlem2  27535  uhgrwkspth  27536  usgr2wlkneq  27537  usgr2trlncl  27541  usgr2pthlem  27544  usgr2pth  27545  cyclnspth  27581  lfgrn1cycl  27583  usgr2trlncrct  27584  uspgrn2crct  27586  crctcshwlkn0lem3  27590  crctcshwlkn0lem5  27592  wwlknp  27621  wspthneq1eq2  27638  0enwwlksnge1  27642  wlklnwwlkln1  27646  wlkiswwlks2  27653  wlkiswwlksupgr2  27655  wlklnwwlkln2lem  27660  wwlksnred  27670  wwlksnextbi  27672  wwlksnredwwlkn0  27674  wwlksnextwrd  27675  wwlksnextinj  27677  wwlksnextproplem3  27690  wwlksnextprop  27691  wspthsnwspthsnon  27695  wspthsnonn0vne  27696  2pthon3v  27722  umgr2adedgwlkonALT  27726  umgr2wlk  27728  umgr2wlkon  27729  umgrwwlks2on  27736  elwspths2on  27739  usgr2wspthons3  27743  elwwlks2  27745  rusgrnumwwlk  27754  clwwlkccatlem  27767  clwlkclwwlklem2a4  27775  clwlkclwwlklem2a  27776  clwlkclwwlklem2  27778  clwlkclwwlkf1lem3  27784  erclwwlkeqlen  27797  clwwlknwwlksn  27816  loopclwwlkn1b  27820  clwwlkf1  27828  wwlksext2clwwlk  27836  eleclclwwlknlem2  27840  umgr2cwwk2dif  27843  eleclclwwlkn  27855  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  clwwlknonwwlknonb  27885  clwwlknonex2lem2  27887  clwwlknonex2  27888  1pthon2v  27932  upgr3v3e3cycl  27959  uhgr3cyclexlem  27960  uhgr3cyclex  27961  eupth2lem3lem4  28010  frgr3vlem1  28052  frgr3vlem2  28053  3vfriswmgrlem  28056  3vfriswmgr  28057  3cyclfrgrrn1  28064  n4cyclfrgr  28070  frgrncvvdeqlem3  28080  frgrncvvdeqlem6  28083  frgrncvvdeqlem7  28084  frgrncvvdeqlem8  28085  frgrwopreglem4a  28089  frgrwopreglem3  28093  frgrwopreg1  28097  frgrwopreg2  28098  frgrwopreglem5lem  28099  frgrwopreglem5ALT  28101  frgrwopreg  28102  fusgr2wsp2nb  28113  2wspmdisj  28116  numclwwlk1lem2foa  28133  numclwwlk1lem2f1  28136  numclwwlk1lem2fo  28137  numclwwlk1  28140  wlkl0  28146  numclwwlk2lem1  28155  numclwlk2lem2f  28156  numclwlk2lem2f1o  28158  frgrreg  28173  frgrregord013  28174  frgrregord13  28175  friendshipgt3  28177  friendship  28178  eulplig  28262  ipassi  28618  ubthlem2  28648  isch3  29018  shintcli  29106  shmodsi  29166  spansncvi  29429  hoaddsub  29593  eigorthi  29614  pjss2coi  29941  pjnormssi  29945  pj3cor1i  29986  strb  30035  dmdmd  30077  mdsl0  30087  csmdsymi  30111  chrelat2i  30142  mdsymlem3  30182  mdsymlem6  30185  sumdmdlem2  30196  opreu2reuALT  30240  ssrelf  30366  spthcycl  32376  loop1cycl  32384  cvmlift2lem1  32549  satfrel  32614  satfrnmapom  32617  fmlafvel  32632  fmla1  32634  gonarlem  32641  gonar  32642  goalrlem  32643  goalr  32644  satffunlem  32648  satffunlem1lem1  32649  satffunlem2lem1  32651  satffun  32656  satefvfmla1  32672  mrsubvrs  32769  mclsax  32816  3ccased  32949  dfon2lem3  33030  rdgprc  33039  trpredmintr  33070  trpredrec  33077  frr3g  33121  sltval2  33163  nolt02o  33199  sslttr  33268  scutun12  33271  cgrextend  33469  btwndiff  33488  btwnconn1lem12  33559  brsegle  33569  broutsideof2  33583  funray  33601  elicc3  33665  nn0prpwlem  33670  nn0prpw  33671  fnessref  33705  neibastop2lem  33708  filnetlem4  33729  meran1  33759  waj-ax  33762  arg-ax  33764  bj-con2com  33896  bj-axdd2  33926  bj-alrimg  33952  bj-exlimg  33956  bj-exalimi  33966  bj-cbvalimt  33972  bj-eximcom  33976  bj-ssbid1ALT  33998  bj-sb  34021  bj-dtru  34139  bj-snsetex  34278  bj-restpw  34386  bj-finsumval0  34570  mptsnunlem  34622  icoreclin  34641  relowlpssretop  34648  inunissunidif  34659  rdgssun  34662  finorwe  34666  domalom  34688  wl-dral1d  34786  wl-exeq  34789  wl-lem-exsb  34817  poimirlem29  34936  poimirlem32  34939  fdc  35035  seqpo  35037  incsequz  35038  isismty  35094  ismtybndlem  35099  heibor1lem  35102  ismgmOLD  35143  isexid2  35148  ghomco  35184  pridlc  35364  relcnveq3  35593  elrelscnveq3  35746  cdleme18d  37446  tendovalco  37916  cdlemn11pre  38361  dihord2pre  38376  nnadddir  39212  incssnn0  39357  fphpd  39462  jm2.19lem3  39637  setindtr  39670  islssfg2  39720  mpaaeu  39799  pr2cv  39956  refimssco  40016  iunrelexpmin1  40102  iunrelexpmin2  40106  trclimalb2  40120  clsk1indlem3  40442  syldbl2  40568  tfindsd  40613  mnurndlem1  40666  nzss  40698  sb5ALT  40908  truniALT  40924  ee223  41017  3orbi123VD  41233  sbc3orgVD  41234  exbirVD  41236  exbiriVD  41237  sbcim2gVD  41258  trsbcVD  41260  truniALTVD  41261  onfrALTlem3VD  41270  onfrALTlem2VD  41272  csbrngVD  41279  19.41rgVD  41285  ax6e2eqVD  41290  ax6e2ndeqVD  41292  2uasbanhVD  41294  sb5ALTVD  41296  vk15.4jVD  41297  infxrunb3rnmpt  41751  stoweidlem26  42360  hirstL-ax3  43177  rexsb  43346  rexrsb  43347  euoreqb  43357  2reu8i  43361  afvres  43420  tz6.12-afv  43421  afvco2  43424  afv2orxorb  43476  afv2res  43487  tz6.12-afv2  43488  tz6.12i-afv2  43491  dfatcolem  43503  zm1nn  43551  fzoopth  43576  2ffzoeq  43577  smonoord  43580  iccpartiltu  43631  iccpartlt  43633  iccpartltu  43634  iccpartgtl  43635  iccpartgt  43636  iccpartleu  43637  iccpartgel  43638  icceuelpart  43645  iccpartnel  43647  lswn0  43653  ichnreuop  43683  ichreuopeq  43684  prsprel  43698  sprsymrelfvlem  43701  sprsymrelf1lem  43702  sprsymrelfolem2  43704  prproropf1olem4  43717  paireqne  43722  prprelb  43727  reupr  43733  goldbachth  43758  odz2prm2pw  43774  fmtno4prmfac  43783  fmtno4prmfac193  43784  prmdvdsfmtnof1lem2  43796  2pwp1prmfmtno  43801  lighneallem2  43820  lighneallem4b  43823  lighneallem4  43824  requad2  43837  odd2prm2  43932  mogoldbblem  43934  gbepos  43972  gbowgt5  43976  gbowge7  43977  stgoldbwt  43990  sbgoldbwt  43991  sbgoldbst  43992  sbgoldbaltlem1  43993  sbgoldbalt  43995  sbgoldbo  44001  nnsum3primesle9  44008  nnsum4primesodd  44010  nnsum4primesoddALTV  44011  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  bgoldbtbndlem1  44019  bgoldbtbndlem2  44020  bgoldbtbndlem3  44021  bgoldbtbnd  44023  isomuspgrlem1  44041  upgrwlkupwlk  44064  uspgrsprf1  44071  mgmhmlin  44102  issubmgm2  44106  lmod0rng  44188  lidldomn1  44241  lidlmmgm  44245  rnghmsscmap  44294  rnghmsubcsetclem2  44296  rngcinv  44301  rngccatidALTV  44309  rngcinvALTV  44313  funcrngcsetc  44318  funcrngcsetcALT  44319  rhmsscmap  44340  rhmsubcsetclem2  44342  rhmsubcrngclem2  44348  ringcinv  44352  ringcbasbas  44354  funcringcsetc  44355  funcringcsetcALTV2lem9  44364  ringccatidALTV  44372  ringcinvALTV  44376  ringcbasbasALTV  44378  rhmsubclem4  44409  rhmsubcALTVlem4  44427  ztprmneprm  44444  pgrpgt2nabl  44463  lmodvsmdi  44479  ply1mulgsumlem2  44490  lincsumcl  44535  ellcoellss  44539  linindslinci  44552  islinindfis  44553  lincext3  44560  lindslinindimp2lem4  44565  lindslinindsimp2lem5  44566  lindslinindsimp2  44567  lindsrng01  44572  ldepspr  44577  lincresunit3lem1  44583  elfzolborelfzop1  44623  dignn0ldlem  44711  nn0sumshdiglem1  44730  rrx2xpref1o  44754  rrx2plord2  44758  rrx2plordisom  44759  line2ylem  44787  line2xlem  44789  line2y  44791  itschlc0xyqsol1  44802  inlinecirc02plem  44822  tfis2d  44832  onsetrec  44859