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  122  con3rr3  152  expt  169  jad  175  pm2.61  183  syl5ibcom  236  syl5ibrcom  238  pm5.501  357  impcom  396  impd  398  expcom  400  expdcom  401  expdOLD  403  simplbi2com  492  imdistanri  561  jaod  877  orel1  904  pm2.62  914  pm2.75  948  pm2.64  956  ccased  1052  dedlem0b  1058  3impd  1450  3expd  1455  mp3an1i  1571  minimp  1715  meredith  1721  19.35  1967  speimfw  2056  sbequ2  2062  equtrr  2118  equeucl  2120  sb56  2283  cbv1  2440  nfeqf2  2464  axc11n  2474  dvelimdf  2497  ax12b  2503  equvel  2505  sbied  2568  exsb  2628  mo2v  2637  euex  2654  exmoeu  2663  mo3  2668  2mo  2713  2eu6  2720  exists2  2724  rexlimdv  3216  r19.12  3249  2gencl  3428  3gencl  3429  rspccv  3497  ceqex  3525  mob  3584  euind  3589  reuind  3607  sseq2  3822  nelss  3859  reupick2  4112  rspn0  4133  disjeq0  4218  uneqdifeq  4251  ssprsseq  4544  preq12b  4567  prel12OLD  4568  prnebg  4574  prel12g  4584  3elpr2eq  4627  iinss2  4762  trintss  4960  dtru  5038  reusv2lem1  5065  alxfr  5074  ralxfrALT  5082  sspwb  5105  copsexg  5143  snopeqop  5158  propeqop  5160  opthhausdorff  5170  opthhausdorff0  5171  pocl  5237  pofun  5246  solin  5253  frss  5276  2optocl  5396  3optocl  5397  ssrel  5407  ssrelOLD  5408  ssrel2  5410  ssrelrel  5420  relop  5472  dfres3  5600  asymref2  5722  xpidtr  5727  trin2  5728  poltletr  5737  xp11  5778  relcnvtr  5867  tz7.7  5960  ordtri3OLD  5971  ordtr2  5979  suc11  6042  iotaval  6073  funmo  6115  fundif  6147  fss  6267  f0dom0  6302  fv3  6424  tz6.12i  6432  mpteqb  6518  fveqdmss  6574  eldmrexrnb  6586  funopsn  6635  funsndifnop  6638  tpres  6689  funfvima  6715  fvclss  6722  f1veqaeq  6736  isoselem  6813  oprabv  6931  ovg  7027  elovmpt3rab1  7121  sorpsscmpl  7176  iunpw  7206  ordom  7302  limom  7308  peano5  7317  fornex  7363  bropopvvv  7487  bropfvvvvlem  7488  f1o2ndf1  7517  poxp  7521  soxp  7522  suppimacnv  7538  ressuppss  7546  ressuppssdif  7548  tposfn2  7607  wfr3g  7646  onnseq  7675  smoel  7691  smogt  7698  smoiso2  7700  tfr3  7729  tz7.48-2  7771  tz7.48-3  7773  tz7.49  7774  oecl  7852  oaordex  7873  oalimcl  7875  oaass  7876  omordi  7881  omlimcl  7893  odi  7894  omeulem1  7897  oen0  7901  nnawordi  7936  nnaass  7937  nnmordi  7946  omabs  7962  omsmolem  7968  iiner  8052  2ecoptocl  8071  3ecoptocl  8072  undifixp  8179  xpdom2  8292  xpf1o  8359  infensuc  8375  php  8381  onomeneq  8387  isinf  8410  findcard2  8437  unblem2  8450  infssuni  8494  finsschain  8510  fsuppunfi  8532  fsuppunbi  8533  marypha1  8577  hartogs  8686  card2on  8696  card2inf  8697  xpwdomg  8727  elirrv  8738  en3lp  8754  preleqg  8755  inf3lem1  8770  inf3lem2  8771  inf3lem3  8772  inf3lem5  8774  noinfep  8802  trcl  8849  tcel  8866  rankonidlem  8936  scottex  8993  djuunxp  9028  eldju2ndl  9031  updjud  9041  dif1card  9114  fodomnum  9161  cardaleph  9193  kmlem9  9263  kmlem13  9267  cflim2  9368  cfsmolem  9375  infpssrlem3  9410  isfin7-2  9501  fin1a2lem6  9510  fin1a2lem10  9514  fin1a2lem12  9516  domtriomlem  9547  axdc3lem4  9558  axdc4lem  9560  zorn2lem3  9603  zorn2lem4  9604  zorn2lem5  9605  zorn2lem7  9607  zornn0g  9610  axdclem2  9625  ondomon  9668  alephval2  9677  cfpwsdom  9689  wuncval2  9852  grupr  9902  gruiun  9904  ingru  9920  grothomex  9934  indpi  10012  nqereu  10034  prlem934  10138  reclem2pr  10153  mulgt0sr  10209  supsrlem  10215  dedekind  10483  lemul1a  11160  squeeze0  11209  peano5nni  11306  nnunb  11553  nn0lt2  11704  nn0le2is012  11705  fzind  11739  nn0ind-raph  11741  zindd  11742  eluzadd  11931  uzin  11936  nn01to3  11998  xnn0xadd0  12293  xmulasslem  12331  icoshft  12513  fzen  12579  uzsubsubfz  12584  elfz0ubfz0  12665  elfz0fzfz0  12666  fz0fzelfz0  12667  elfzmlbp  12672  elfzodifsumelfzo  12756  ssfzo12bi  12785  elfzonelfzo  12792  elfznelfzo  12795  injresinjlem  12810  injresinj  12811  modfzo0difsn  12964  modsumfzodifsn  12965  addmodlteq  12967  ssnn0fi  13006  fsuppmapnn0fiub0  13014  expcllem  13092  expeq0  13111  mulexp  13120  leexp2r  13139  bernneq  13211  facdiv  13292  hasheqf1oi  13358  hashnn0n0nn  13396  hashss  13412  hashgt12el  13425  hashgt12el2  13426  hashimarni  13443  hash2prde  13467  hashle2pr  13474  pr2pwpr  13476  hashge2el2dif  13477  hashge2el2difr  13478  hashtpg  13482  hashge3el3dif  13483  exprelprel  13486  hash1to3  13488  fundmge2nop0  13489  fi1uzind  13494  ccatsymb  13577  swrdnd  13654  swrdnd2  13655  swrdswrdlem  13681  swrdswrd  13682  swrdccatin1  13705  swrdccatin12lem2a  13707  swrdccatin12lem2b  13708  swrdccatin2  13709  swrdccatin12lem2  13711  swrdccatin12lem3  13712  swrdccat3  13714  swrdccat  13715  swrdccat3blem  13717  repsdf2  13747  repswswrd  13753  cshwidxmod  13771  cshwidx0  13774  cshf1  13778  2cshw  13781  cshweqrep  13789  cshw1  13790  cshwsexa  13792  2cshwcshw  13793  scshwfzeqfzo  13794  cshwcsh2id  13796  swrdco  13805  wwlktovfo  13924  relexpaddg  14014  cjexp  14111  absexp  14265  iseraltlem2  14634  modfsummods  14745  clim2prod  14839  prodfn0  14845  prodfrec  14846  prodmo  14885  fprodabs  14923  binomfallfac  14990  fprodefsum  15043  dvdsaddre2b  15250  addmodlteqALT  15268  oddge22np1  15291  nn0enne  15312  nn0o1gt2  15315  sumeven  15328  sumodd  15329  dvdslegcd  15443  gcdneg  15460  dfgcd2  15480  rplpwr  15493  lcmf  15563  lcmftp  15566  lcmfunsnlem2lem1  15568  lcmfunsnlem2  15570  lcmfdvds  15572  lcmfdvdsb  15573  lcmfunsn  15574  coprmdvds1  15582  qredeq  15587  coprmprod  15591  coprmproddvdslem  15592  cncongr1  15597  cncongr2  15598  prm2orodd  15620  nnnn0modprm0  15726  prm23lt5  15734  prm23ge5  15735  dvdsprmpweqnn  15804  dvdsprmpweqle  15805  oddprmdvds  15822  prmpwdvds  15823  prmreclem4  15838  ramcl  15948  prmgaplem6  15975  prmgaplem7  15976  prmgaplem8  15977  cshwshashlem1  16012  cshwshashlem2  16013  cshwshashlem3  16014  cshwrepswhash1  16019  setsn0fun  16104  setsstruct2  16105  setsstructOLD  16108  imasleval  16404  mreiincl  16459  mreexexd  16511  inveq  16636  cicsym  16666  cictr  16667  initoid  16857  termoid  16858  initoeu2lem0  16865  initoeu2lem1  16866  initoeu2lem2  16867  initoeu2  16868  fthestrcsetc  16993  fthsetcestrc  17008  drsdirfi  17141  isnmgm  17449  sgrpass  17493  mgm2nsgrplem3  17610  dfgrp3lem  17716  symg2bas  18017  symgfix2  18035  symgextf1  18040  gsmsymgrfix  18047  pmtrprfv3  18073  psgnunilem4  18116  efgi2  18337  lmodvsmmulgdi  19100  0ringnnzr  19476  mpfrcl  19724  gsummoncoe1  19880  psgndiflemB  20152  psgndiflemA  20153  elfrlmbasn0  20314  lmictra  20392  mamufacex  20403  matecl  20439  dmatelnd  20511  dmatscmcl  20518  scmateALT  20527  scmatsgrp1  20537  scmatf1  20546  mavmulsolcl  20566  cramerimplem1  20699  cramerimplem1OLD  20700  cramerimplem2  20701  pmatcollpw3fi1  20804  mp2pm2mplem4  20825  pm2mpfo  20830  chmaidscmat  20864  fvmptnn04ifb  20867  chfacfscmul0  20874  chfacfpmmul0  20878  cayhamlem1  20882  cayhamlem3  20903  cayleyhamilton1  20908  fiinopn  20917  toprntopon  20941  tgcl  20985  distop  21011  isclo2  21104  iscldtop  21111  ssnei2  21132  opnnei  21136  pnfnei  21236  mnfnei  21237  tgcnp  21269  cnpnei  21280  1stcelcls  21476  txcnpi  21623  cnmptcom  21693  fbfinnfr  21856  isfildlem  21872  snfil  21879  fbunfip  21884  fgcl  21893  elfm2  21963  fmco  21976  fbflim2  21992  cnpflf2  22015  flimfcls  22041  tmdgsum  22110  neibl  22517  tngngpim  22674  fgcfil  23279  caubl  23316  volsuplem  23534  ellimc3  23855  dvnadd  23904  dvnres  23906  cpnord  23910  dvnfre  23927  ply1divex  24108  cxpmul2  24647  zabsle1  25233  gausslemma2dlem0i  25301  gausslemma2dlem1a  25302  gausslemma2dlem3  25305  lgsquad2lem2  25322  2lgs  25344  qabvexp  25527  axcontlem4  26059  umgredgprv  26214  umgrnloop  26215  upgrpredgv  26247  upgredgpr  26250  edglnl  26251  usgredgprvALT  26300  usgrnloopALT  26308  usgredg2v  26332  fusgrfis  26436  nbuhgr2vtx1edgblem  26461  nb3grprlem1  26496  cusgrsize2inds  26575  cusgrfi  26580  fusgrn0degnn0  26621  uspgrloopvtxel  26638  vtxdginducedm1lem4  26664  uhgr0edg0rgrb  26696  wlkl1loop  26760  wlk1walk  26761  upgriswlk  26763  upgrwlkvtxedg  26767  uspgr2wlkeq  26768  wlkv0  26773  wlklenvclwlk  26777  wlksoneq1eq2  26786  wlkon2n0  26788  wlkreslem  26792  wlkres  26793  lfgrwlkprop  26810  pthdivtx  26851  2pthnloop  26853  spthonepeq  26874  uhgrwkspthlem2  26876  uhgrwkspth  26877  usgr2wlkneq  26878  usgr2trlncl  26882  usgr2pthlem  26885  usgr2pth  26886  cyclnspth  26922  lfgrn1cycl  26924  usgr2trlncrct  26925  uspgrn2crct  26927  crctcshwlkn0lem3  26931  crctcshwlkn0lem5  26933  wwlknp  26962  wspthneq1eq2  26985  0enwwlksnge1  26989  wlklnwwlkln1  26993  wlkiswwlks2  27000  wlkiswwlksupgr2  27002  wlklnwwlkln2lem  27007  wwlksnred  27027  wwlksnext  27028  wwlksnextbi  27029  wwlksnredwwlkn0  27031  wwlksnextwrd  27032  wwlksnextinj  27034  wwlksnextproplem3  27047  wwlksnextprop  27048  wspthsnwspthsnon  27052  wspthsnwspthsnonOLD  27054  wspthsnonn0vne  27055  2pthon3v  27081  umgr2adedgwlkonALT  27085  umgr2wlk  27087  umgr2wlkon  27088  elwwlks2ons3OLD  27094  umgrwwlks2on  27096  elwspths2on  27099  usgr2wspthons3  27104  elwwlks2  27106  rusgrnumwwlk  27115  clwwlknclwwlkdifsOLD  27120  clwwlkccatlem  27130  clwwlkccat  27131  clwlkclwwlklem2a4  27138  clwlkclwwlklem2a  27139  clwlkclwwlklem2  27141  clwlkclwwlkf1lem3  27147  erclwwlkeqlen  27160  clwwlknwwlksn  27184  clwwlknwwlksnOLD  27185  loopclwwlkn1b  27189  clwwlkf1  27196  wwlksext2clwwlk  27205  wwlksext2clwwlkOLD  27206  eleclclwwlknlem2  27210  umgr2cwwk2dif  27213  eleclclwwlkn  27225  hashecclwwlkn1  27226  umgrhashecclwwlk  27227  clwlksfclwwlkOLD  27234  clwlksfoclwwlkOLD  27235  clwwlknonwwlknonb  27272  clwwlknonex2lem2  27275  clwwlknonex2  27276  clwwlknunOLD  27284  1pthon2v  27324  upgr3v3e3cycl  27351  uhgr3cyclexlem  27352  uhgr3cyclex  27353  eupth2lem3lem4  27402  frgr3vlem1  27446  frgr3vlem2  27447  3vfriswmgrlem  27450  3vfriswmgr  27451  3cyclfrgrrn1  27458  n4cyclfrgr  27464  frgrncvvdeqlem3  27474  frgrncvvdeqlem6  27477  frgrncvvdeqlem7  27478  frgrncvvdeqlem8  27479  frgrwopreglem4a  27483  frgrwopreglem3  27487  frgrwopreg1  27491  frgrwopreg2  27492  frgrwopreglem5lem  27493  frgrwopreglem5ALT  27495  frgrwopreg  27496  fusgr2wsp2nb  27507  2wspmdisj  27510  numclwwlk1lem2foa  27531  numclwwlk1lem2f1  27534  numclwwlk1lem2fo  27535  numclwwlk1  27539  wlkl0  27545  numclwwlk2lem1  27554  numclwlk2lem2f  27555  numclwlk2lem2f1o  27557  numclwwlk2lem1OLD  27561  numclwlk2lem2fOLD  27562  numclwlk2lem2f1oOLD  27564  frgrreg  27580  frgrregord013  27581  frgrregord13  27582  friendshipgt3  27584  friendship  27585  eulplig  27666  ipassi  28022  ubthlem2  28053  isch3  28424  shintcli  28514  shmodsi  28574  spansncvi  28837  hoaddsub  29001  eigorthi  29022  pjss2coi  29349  pjnormssi  29353  pj3cor1i  29394  strb  29443  dmdmd  29485  mdsl0  29495  csmdsymi  29519  chrelat2i  29550  mdsymlem3  29590  mdsymlem6  29593  sumdmdlem2  29604  ssrelf  29750  cvmlift2lem1  31605  mrsubvrs  31740  mclsax  31787  3ccased  31920  dfon2lem3  32008  rdgprc  32018  trpredmintr  32049  trpredrec  32056  frr3g  32098  sltval2  32128  nolt02o  32164  sslttr  32233  scutun12  32236  cgrextend  32434  btwndiff  32453  btwnconn1lem12  32524  brsegle  32534  broutsideof2  32548  funray  32566  elicc3  32630  nn0prpwlem  32636  nn0prpw  32637  fnessref  32671  neibastop2lem  32674  filnetlem4  32695  meran1  32725  waj-ax  32728  arg-ax  32730  bj-con2com  32860  bj-axdd2  32889  bj-exalimi  32925  bj-ssbequ2  32956  bj-ssbequ1  32957  bj-ssbid1ALT  32961  bj-sb  32990  bj-cbv1v  33041  bj-dtru  33109  bj-mo3OLD  33143  bj-snsetex  33259  bj-restpw  33354  bj-finsumval0  33462  mptsnunlem  33500  icoreclin  33519  relowlpssretop  33526  wl-dral1d  33630  wl-exeq  33633  wl-lem-exsb  33660  poimirlem29  33749  poimirlem32  33752  fdc  33850  seqpo  33852  incsequz  33853  isismty  33909  ismtybndlem  33914  heibor1lem  33917  ismgmOLD  33958  isexid2  33963  ghomco  33999  pridlc  34179  relcnveq3  34405  elrelscnveq3  34552  cdleme18d  36074  tendovalco  36544  cdlemn11pre  36989  dihord2pre  37004  incssnn0  37774  fphpd  37880  jm2.19lem3  38057  setindtr  38090  islssfg2  38140  mpaaeu  38219  refimssco  38411  iunrelexpmin1  38498  iunrelexpmin2  38502  trclimalb2  38516  clsk1indlem3  38839  syldbl2  38966  nzss  39014  sb5ALT  39227  truniALT  39247  ee223  39355  3orbi123VD  39577  sbc3orgVD  39578  exbirVD  39580  exbiriVD  39581  sbcim2gVD  39603  trsbcVD  39605  truniALTVD  39606  onfrALTlem3VD  39615  onfrALTlem2VD  39617  csbrngVD  39624  19.41rgVD  39630  ax6e2eqVD  39635  ax6e2ndeqVD  39637  2uasbanhVD  39639  sb5ALTVD  39641  vk15.4jVD  39642  infxrunb3rnmpt  40132  stoweidlem26  40720  hirstL-ax3  41539  rexsb  41679  rexrsb  41680  2reu1  41696  afvres  41759  tz6.12-afv  41760  afvco2  41763  afv2orxorb  41815  afv2res  41826  tz6.12-afv2  41827  tz6.12i-afv2  41830  dfatcolem  41842  zm1nn  41890  fzoopth  41910  2ffzoeq  41911  smonoord  41914  iccpartiltu  41931  iccpartlt  41933  iccpartltu  41934  iccpartgtl  41935  iccpartgt  41936  iccpartleu  41937  iccpartgel  41938  icceuelpart  41945  iccpartnel  41947  lswn0  41953  pfxccatin12lem1  41996  pfxccatin12lem2  41997  pfxccat3  41999  goldbachth  42032  odz2prm2pw  42048  fmtno4prmfac  42057  fmtno4prmfac193  42058  prmdvdsfmtnof1lem2  42070  2pwp1prmfmtno  42077  lighneallem2  42096  lighneallem4b  42099  lighneallem4  42100  odd2prm2  42200  mogoldbblem  42202  gbepos  42219  gbowgt5  42223  gbowge7  42224  stgoldbwt  42237  sbgoldbwt  42238  sbgoldbst  42239  sbgoldbaltlem1  42240  sbgoldbalt  42242  sbgoldbo  42248  nnsum3primesle9  42255  nnsum4primesodd  42257  nnsum4primesoddALTV  42258  nnsum4primeseven  42261  nnsum4primesevenALTV  42262  bgoldbtbndlem1  42266  bgoldbtbndlem2  42267  bgoldbtbndlem3  42268  bgoldbtbnd  42270  upgrwlkupwlk  42287  prsprel  42303  sprsymrelfvlem  42306  sprsymrelf1lem  42307  sprsymrelfolem2  42309  uspgrsprf1  42321  mgmhmlin  42352  issubmgm2  42356  lmod0rng  42434  lidldomn1  42487  lidlmmgm  42491  rnghmsscmap  42540  rnghmsubcsetclem2  42542  rngcinv  42547  rngccatidALTV  42555  rngcinvALTV  42559  funcrngcsetc  42564  funcrngcsetcALT  42565  rhmsscmap  42586  rhmsubcsetclem2  42588  rhmsubcrngclem2  42594  ringcinv  42598  ringcbasbas  42600  funcringcsetc  42601  funcringcsetcALTV2lem9  42610  ringccatidALTV  42618  ringcinvALTV  42622  ringcbasbasALTV  42624  rhmsubclem4  42655  rhmsubcALTVlem4  42673  ztprmneprm  42691  pgrpgt2nabl  42713  lmodvsmdi  42729  ply1mulgsumlem2  42741  lincsumcl  42786  ellcoellss  42790  linindslinci  42803  islinindfis  42804  lincext3  42811  lindslinindimp2lem4  42816  lindslinindsimp2lem5  42817  lindslinindsimp2  42818  lindsrng01  42823  ldepspr  42828  lincresunit3lem1  42834  elfzolborelfzop1  42875  dignn0ldlem  42962  nn0sumshdiglem1  42981  tfis2d  42993  onsetrec  43020