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  exptOLD  178  jad  188  pm2.61  193  syl5ibcom  246  syl5ibrcom  248  pm5.501  367  impcom  408  impd  411  expcom  414  expdcom  415  simplbi2com  503  imdistanri  574  syldbl2  847  jaod  865  orel1  894  pm2.62  905  pm2.75  939  pm2.64  949  ccased  1044  dedlem0b  1050  3impd  1355  3expd  1360  mp3an1i  1462  minimp  1628  meredith  1648  19.35  1884  speimfw  1970  equtrr  2029  equeucl  2031  ax12ev2  2192  sbiedw  2325  cbv1v  2344  exsb  2367  cbv1  2410  ax12b  2432  axc11n  2434  dvelimdf  2457  equvel  2464  dfsb1  2489  sbied  2511  dfmoeu  2539  mo3  2568  mo4  2570  2mo  2652  2eu6  2661  exists2  2666  pm2.61dne  3021  rexlimdv  3139  r19.21v  3165  r19.12  3289  2gencl  3475  3gencl  3476  vtocl2ga  3524  vtocl2gaf  3525  vtocl3gaf  3527  vtocl3ga  3529  vtocl4ga  3532  rspccv  3564  ceqex  3597  mob  3665  euind  3672  reuind  3701  2reu1  3836  sseq2  3948  nelss  3987  rexdifi  4087  reupick2  4266  disjeq0  4391  uneqdifeq  4427  sspw  4547  ssprsseq  4763  preq12b  4788  prnebg  4794  prel12g  4802  3elpr2eq  4844  iinss2  4994  trintss  5205  dtruALT2  5306  reusv2lem1  5334  alxfr  5343  ralxfrALT  5351  exexneq  5381  copsexgw  5437  copsexgwOLD  5438  copsexg  5439  snopeqop  5454  propeqop  5455  opthhausdorff  5465  opthhausdorff0  5466  pofun  5551  solin  5560  frss  5589  2optocl  5721  3optocl  5722  ssrel  5733  ssrel2  5735  ssrelrel  5746  relop  5799  dfres3  5943  asymref2  6074  xpidtr  6079  trin2  6080  poltletr  6089  imadifssran  6109  xp11  6133  relcnvtrg  6225  reuop  6251  tz7.7  6343  ordtr2  6362  suc11  6426  fundif  6541  fss  6678  f0dom0  6718  fv3  6852  tz6.12i  6860  mpteqb  6962  fveqdmss  7026  eldmrexrnb  7040  funopsnOLD  7098  funsndifnop  7101  tpres  7152  funfvima  7181  fvclss  7192  f1veqaeq  7207  fvf1pr  7258  isoselem  7292  oprabv  7423  ovg  7528  elovmpt3rab1  7623  sorpsscmpl  7684  iunpw  7721  trom  7822  limom  7829  peano5  7840  focdmex  7905  funelss  7996  funeldmdif  7997  bropopvvv  8036  bropfvvvvlem  8037  f1o2ndf1  8068  poxp  8075  soxp  8076  poxp2  8090  frxp2  8091  frxp3  8098  suppimacnv  8121  ressuppss  8130  ressuppssdif  8132  tposfn2  8195  wfr3g  8266  onnseq  8281  smoel  8297  smogt  8304  smoiso2  8306  tfr3  8335  tz7.48-2  8378  tz7.48-3  8380  tz7.49  8381  oecl  8469  oaordex  8490  oalimcl  8492  oaass  8493  omordi  8498  omlimcl  8510  odi  8511  omeulem1  8514  oen0  8519  nnawordi  8554  nnaass  8555  nnmordi  8564  omabs  8584  omsmolem  8590  naddssim  8618  brinxper  8670  iiner  8733  2ecoptocl  8752  3ecoptocl  8753  undifixp  8879  xpdom2  9007  xpf1o  9074  infensuc  9090  findcard2  9096  php  9138  isinf  9172  unblem2  9200  fodomfir  9235  infssuni  9253  finsschain  9266  fsuppunfi  9298  fsuppunbi  9299  marypha1  9344  hartogs  9456  card2on  9466  card2inf  9467  xpwdomg  9497  elirrvOLD  9510  elirrvOLDOLD  9511  en3lp  9533  preleqg  9534  inf3lem1  9547  inf3lem2  9548  inf3lem3  9549  inf3lem5  9551  noinfep  9579  ttrclss  9639  ttrclselem2  9645  trcl  9647  tcel  9662  frr3g  9678  rankonidlem  9750  scottex  9807  djuunxp  9843  eldju2ndl  9846  updjud  9856  dif1card  9930  fodomnum  9977  cardaleph  10009  kmlem9  10079  kmlem13  10083  cflim2  10183  cfsmolem  10190  infpssrlem3  10225  isfin7-2  10316  fin1a2lem6  10325  fin1a2lem12  10331  domtriomlem  10362  axdc3lem4  10373  axdc4lem  10375  zorn2lem3  10418  zorn2lem4  10419  zorn2lem5  10420  zorn2lem7  10422  zornn0g  10425  axdclem2  10440  ondomon  10483  alephval2  10493  cfpwsdom  10505  wuncval2  10668  grupr  10718  gruiun  10720  ingru  10736  grothomex  10750  indpi  10828  nqereu  10850  prlem934  10954  reclem2pr  10969  mulgt0sr  11026  supsrlem  11032  1re  11142  dedekind  11307  lemul1a  12007  squeeze0  12057  peano5nni  12175  nnadddir  12231  nnunb  12431  nn0lt2  12590  nn0le2is012  12591  fzind  12625  nn0ind-raph  12627  zindd  12628  uzin  12822  nn01to3  12889  xnn0xadd0  13197  xmulasslem  13235  icoshft  13424  fzen  13493  uzsubsubfz  13498  elfz0ubfz0  13584  elfz0fzfz0  13585  fz0fzelfz0  13586  elfzmlbp  13591  elfzodifsumelfzo  13684  ssfzo12bi  13714  fzoopth  13715  elfzonelfzo  13722  elfznelfzo  13726  injresinjlem  13743  injresinj  13744  modfzo0difsn  13903  modsumfzodifsn  13904  addmodlteq  13906  ssnn0fi  13945  fsuppmapnn0fiub0  13953  expcllem  14032  expeq0  14052  mulexp  14061  leexp2r  14134  bernneq  14189  facdiv  14247  hasheqf1oi  14311  hashnn0n0nn  14351  hashss  14369  hashgt12el  14382  hashgt12el2  14383  hashimarni  14401  hashle2pr  14437  pr2pwpr  14439  hashge2el2dif  14440  hashge2el2difr  14441  hashtpg  14445  hashge3el3dif  14447  exprelprel  14450  hash1to3  14452  hash3tpde  14453  tpfo  14460  fundmge2nop0  14462  fi1uzind  14467  ccatsymb  14543  swrdnd  14615  swrdnd2  14616  swrdnnn0nd  14617  swrdnd0  14618  pfxnd0  14649  swrdswrdlem  14664  swrdswrd  14665  pfxccatin12lem2a  14687  pfxccatin12lem1  14688  swrdccatin2  14689  pfxccatin12lem2  14691  pfxccatin12lem3  14692  pfxccat3  14694  swrdccat  14695  swrdccat3blem  14699  repsdf2  14738  repswswrd  14744  cshwidxmod  14763  cshwidx0  14766  cshf1  14770  cshweqrep  14781  cshw1  14782  2cshwcshw  14785  scshwfzeqfzo  14786  cshwcsh2id  14788  wwlktovfo  14918  relexpaddg  15013  iseraltlem2  15643  modfsummods  15754  clim2prod  15851  prodfn0  15857  prodfrec  15858  prodmo  15899  fprodabs  15937  binomfallfac  16004  fprodefsum  16058  dvdsaddre2b  16274  addmodlteqALT  16292  oddge22np1  16316  nn0enne  16344  nn0o1gt2  16348  sumeven  16354  sumodd  16355  dvdslegcd  16471  gcdneg  16489  dfgcd2  16513  rplpwr  16525  lcmf  16600  lcmftp  16603  lcmfunsnlem2lem1  16605  lcmfunsnlem2  16607  lcmfdvdsb  16610  coprmdvds1  16619  qredeq  16624  coprmprod  16628  coprmproddvdslem  16629  cncongr1  16634  cncongr2  16635  prm2orodd  16658  2mulprm  16660  nnnn0modprm0  16775  prm23lt5  16783  prm23ge5  16784  dvdsprmpweqnn  16854  dvdsprmpweqle  16855  oddprmdvds  16872  prmpwdvds  16873  prmreclem4  16888  ramcl  16998  prmgaplem6  17025  prmgaplem7  17026  prmgaplem8  17027  cshwshashlem1  17064  cshwshashlem2  17065  cshwshashlem3  17066  cshwrepswhash1  17071  setsn0fun  17141  setsstruct2  17142  imasleval  17503  mreiincl  17556  mreexexd  17612  inveq  17739  cicsym  17769  cictr  17770  initoid  17966  termoid  17967  initoeu2lem0  17978  initoeu2lem1  17979  initoeu2lem2  17980  initoeu2  17981  fthestrcsetc  18114  fthsetcestrc  18129  drsdirfi  18269  isnmgm  18610  mgmhmlin  18665  issubmgm2  18669  sgrpass  18691  insubm  18784  mgm2nsgrplem3  18889  dfgrp3lem  19012  cyccom  19176  symg2bas  19366  symgfix2  19389  symgextf1  19394  gsmsymgrfix  19401  pmtrprfv3  19427  psgnunilem4  19470  efgi2  19698  0ringnnzr  20504  rnghmsscmap  20609  rnghmsubcsetclem2  20611  rngcinv  20616  funcrngcsetc  20619  funcrngcsetcALT  20620  rhmsscmap  20638  rhmsubcsetclem2  20640  rhmsubcrngclem2  20646  ringcbasbas  20652  funcringcsetc  20653  rhmsubclem4  20667  rngqiprngimfo  21301  psgndiflemB  21582  psgndiflemA  21583  elfrlmbasn0  21745  lmictra  21827  mpfrcl  22068  gsummoncoe1  22301  mamufacex  22386  matecl  22415  dmatelnd  22486  dmatscmcl  22493  scmateALT  22502  scmatsgrp1  22512  scmatf1  22521  mavmulsolcl  22541  cramerimplem1  22673  cramerimplem2  22674  pmatcollpw3fi1  22778  mp2pm2mplem4  22799  pm2mpfo  22804  chmaidscmat  22838  fvmptnn04ifb  22841  chfacfscmul0  22848  chfacfpmmul0  22852  cayhamlem1  22856  cayhamlem3  22877  cayleyhamilton1  22882  fiinopn  22891  tgcl  22959  distop  22985  isclo2  23078  iscldtop  23085  ssnei2  23106  opnnei  23110  pnfnei  23210  mnfnei  23211  tgcnp  23243  cnpnei  23254  1stcelcls  23451  txcnpi  23598  cnmptcom  23668  fbfinnfr  23831  isfildlem  23847  snfil  23854  fbunfip  23859  fgcl  23868  elfm2  23938  fmco  23951  fbflim2  23967  cnpflf2  23990  flimfcls  24016  tmdgsum  24085  neibl  24491  tngngpim  24649  fgcfil  25263  caubl  25300  volsuplem  25547  ellimc3  25871  dvnadd  25921  dvnres  25923  cpnord  25927  dvnfre  25944  ply1divex  26127  cxpmul2  26678  fsumdvdsmul  27183  zabsle1  27284  gausslemma2dlem1a  27353  gausslemma2dlem3  27356  lgsquad2lem2  27373  2lgs  27395  2sq2  27421  2sqnn0  27426  2sqnn  27427  2sqreultlem  27435  2sqreunnltlem  27438  qabvexp  27614  ltsval2  27645  nolt02o  27684  sltsun1  27805  cutsun12  27807  madebday  27917  mulsprop  28147  precsexlem8  28231  precsexlem9  28232  noseqind  28309  om2noseqrdg  28321  n0cutlt  28376  peano5uzs  28421  expadds  28452  bdaypw2n0bndlem  28480  bdaypw2n0bnd  28481  axcontlem4  29061  umgredgprv  29201  umgrnloop  29202  upgrpredgv  29233  upgredgpr  29236  edglnl  29237  usgredgprvALT  29289  usgrnloopALT  29297  usgredg2v  29321  fusgrfis  29424  nbuhgr2vtx1edgblem  29445  nb3grprlem1  29474  cusgrsize2inds  29547  cusgrfi  29552  fusgrn0degnn0  29593  uspgrloopvtxel  29610  vtxdginducedm1lem4  29636  uhgr0edg0rgrb  29668  wlkl1loop  29731  wlk1walk  29732  upgriswlk  29734  upgrwlkvtxedg  29738  uspgr2wlkeq  29739  wlkv0  29743  wlksoneq1eq2  29756  wlkon2n0  29758  wlkreslem  29761  wlkres  29762  lfgrwlkprop  29779  pthdivtx  29820  2pthnloop  29824  spthonepeq  29845  uhgrwkspthlem2  29847  uhgrwkspth  29848  usgr2wlkneq  29849  usgr2trlncl  29853  usgr2pthlem  29856  usgr2pth  29857  cyclnspth  29894  lfgrn1cycl  29898  usgr2trlncrct  29899  uspgrn2crct  29901  crctcshwlkn0lem3  29905  crctcshwlkn0lem5  29907  wwlknp  29936  wspthneq1eq2  29953  0enwwlksnge1  29957  wlklnwwlkln1  29961  wlkiswwlks2  29968  wlkiswwlksupgr2  29970  wlklnwwlkln2lem  29975  wwlksnred  29985  wwlksnextbi  29987  wwlksnredwwlkn0  29989  wwlksnextwrd  29990  wwlksnextinj  29992  wwlksnextproplem3  30004  wwlksnextprop  30005  wspthsnwspthsnon  30009  wspthsnonn0vne  30010  2pthon3v  30036  umgr2adedgwlkonALT  30040  umgr2wlk  30042  umgr2wlkon  30043  usgrwwlks2on  30051  umgrwwlks2on  30052  elwspths2on  30055  elwspths2onw  30056  usgr2wspthons3  30060  elwwlks2  30062  rusgrnumwwlk  30071  clwwlkccatlem  30084  clwlkclwwlklem2a4  30092  clwlkclwwlklem2a  30093  clwlkclwwlklem2  30095  clwlkclwwlkf1lem3  30101  erclwwlkeqlen  30114  clwwlknwwlksn  30133  loopclwwlkn1b  30137  clwwlkf1  30144  wwlksext2clwwlk  30152  eleclclwwlknlem2  30156  umgr2cwwk2dif  30159  eleclclwwlkn  30171  hashecclwwlkn1  30172  umgrhashecclwwlk  30173  clwwlknonwwlknonb  30201  clwwlknonex2lem2  30203  clwwlknonex2  30204  1pthon2v  30248  upgr3v3e3cycl  30275  uhgr3cyclexlem  30276  uhgr3cyclex  30277  eupth2lem3lem4  30326  frgr3vlem1  30368  frgr3vlem2  30369  3vfriswmgrlem  30372  3vfriswmgr  30373  3cyclfrgrrn1  30380  n4cyclfrgr  30386  frgrncvvdeqlem3  30396  frgrncvvdeqlem6  30399  frgrncvvdeqlem7  30400  frgrncvvdeqlem8  30401  frgrwopreglem4a  30405  frgrwopreglem3  30409  frgrwopreg1  30413  frgrwopreg2  30414  frgrwopreglem5lem  30415  frgrwopreglem5ALT  30417  frgrwopreg  30418  fusgr2wsp2nb  30429  2wspmdisj  30432  numclwwlk1lem2foa  30449  numclwwlk1lem2f1  30452  numclwwlk1lem2fo  30453  numclwwlk1  30456  wlkl0  30462  numclwwlk2lem1  30471  numclwlk2lem2f  30472  numclwlk2lem2f1o  30474  frgrreg  30489  frgrregord013  30490  frgrregord13  30491  friendshipgt3  30493  friendship  30494  eulplig  30581  ipassi  30937  ubthlem2  30967  isch3  31337  shintcli  31425  shmodsi  31485  spansncvi  31748  hoaddsub  31912  eigorthi  31933  pjss2coi  32260  pjnormssi  32264  pj3cor1i  32305  strb  32354  dmdmd  32396  mdsl0  32406  csmdsymi  32430  chrelat2i  32461  mdsymlem3  32501  mdsymlem6  32504  sumdmdlem2  32515  opreu2reuALT  32571  ssrelf  32714  gsumwun  33164  r1filim  35292  trssfir1om  35299  fineqvinfep  35313  trssfir1omregs  35324  onvf1odlem4  35341  spthcycl  35364  loop1cycl  35372  cvmlift2lem1  35537  satfrel  35602  satfrnmapom  35605  fmlafvel  35620  fmla1  35622  gonarlem  35629  gonar  35630  goalrlem  35631  goalr  35632  satffunlem  35636  satffunlem1lem1  35637  satffunlem2lem1  35639  satffun  35644  satefvfmla1  35660  mrsubvrs  35757  mclsax  35804  3ccased  35954  dfon2lem3  36018  rdgprc  36027  cgrextend  36243  btwndiff  36262  btwnconn1lem12  36333  brsegle  36343  broutsideof2  36357  funray  36375  in-ax8  36459  ss-ax8  36460  elicc3  36552  nn0prpwlem  36557  nn0prpw  36558  fnessref  36592  neibastop2lem  36595  filnetlem4  36616  meran1  36646  waj-ax  36649  arg-ax  36651  axtco1from2  36710  dfttc4  36765  mh-inf3f1  36776  mh-regprimbi  36780  bj-nnclavc  36861  bj-con2com  36878  bj-axdd2  36910  bj-alrimg  36931  bj-exlimg  36953  bj-exalimi  36963  bj-eximcom  36964  bj-ssbid1ALT  37012  bj-sb  37037  bj-snsetex  37323  bj-axseprep  37434  bj-axreprepsep  37435  bj-restpw  37457  bj-finsumval0  37652  mptsnunlem  37707  icoreclin  37726  relowlpssretop  37733  inunissunidif  37744  rdgssun  37747  finorwe  37751  domalom  37773  wl-dral1d  37909  wl-exeq  37912  wl-lem-exsb  37944  wl-eujustlem1  37966  poimirlem29  38023  poimirlem32  38026  fdc  38119  seqpo  38121  incsequz  38122  isismty  38175  ismtybndlem  38180  heibor1lem  38183  ismgmOLD  38224  isexid2  38229  ghomco  38265  pridlc  38445  relcnveq3  38701  elrelscnveq3  39001  cdleme18d  40794  tendovalco  41264  cdlemn11pre  41709  dihord2pre  41724  indstrd  42685  unitscyglem3  42689  eu6w  43133  incssnn0  43167  fphpd  43268  jm2.19lem3  43443  setindtr  43476  islssfg2  43523  mpaaeu  43602  ordnexbtwnsuc  43719  oaabsb  43746  succlg  43780  oacl2g  43782  omabs2  43784  omcl2  43785  omcl3g  43786  pr2cv  43999  refimssco  44058  iunrelexpmin1  44159  iunrelexpmin2  44163  trclimalb2  44177  clsk1indlem3  44494  tfindsd  44661  mnurndlem1  44732  nzss  44768  sb5ALT  44976  truniALT  44992  ee223  45085  3orbi123VD  45300  sbc3orgVD  45301  exbirVD  45303  exbiriVD  45304  sbcim2gVD  45325  trsbcVD  45327  truniALTVD  45328  onfrALTlem3VD  45337  onfrALTlem2VD  45339  csbrngVD  45346  19.41rgVD  45352  ax6e2eqVD  45357  ax6e2ndeqVD  45359  2uasbanhVD  45361  sb5ALTVD  45363  vk15.4jVD  45364  infxrunb3rnmpt  45878  stoweidlem26  46476  et-equeucl  47322  hirstL-ax3  47362  rexsb  47569  rexrsb  47570  euoreqb  47579  2reu8i  47583  afvres  47642  tz6.12-afv  47643  afvco2  47646  afv2orxorb  47698  afv2res  47709  tz6.12-afv2  47710  tz6.12i-afv2  47713  dfatcolem  47725  zm1nn  47772  2ffzoeq  47798  smonoord  47847  iccpartiltu  47904  iccpartlt  47906  iccpartltu  47907  iccpartgtl  47908  iccpartgt  47909  iccpartleu  47910  iccpartgel  47911  icceuelpart  47918  iccpartnel  47920  lswn0  47926  ichnreuop  47954  ichreuopeq  47955  prsprel  47969  sprsymrelfvlem  47972  sprsymrelf1lem  47973  sprsymrelfolem2  47975  prproropf1olem4  47988  paireqne  47993  prprelb  47998  reupr  48004  goldbachth  48032  odz2prm2pw  48048  fmtno4prmfac  48057  fmtno4prmfac193  48058  prmdvdsfmtnof1lem2  48070  2pwp1prmfmtno  48075  lighneallem2  48091  lighneallem4b  48094  lighneallem4  48095  requad2  48121  odd2prm2  48216  mogoldbblem  48218  gbepos  48256  gbowgt5  48260  gbowge7  48261  stgoldbwt  48274  sbgoldbwt  48275  sbgoldbst  48276  sbgoldbaltlem1  48277  sbgoldbalt  48279  sbgoldbo  48285  nnsum3primesle9  48292  nnsum4primesodd  48294  nnsum4primesoddALTV  48295  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  bgoldbtbndlem1  48303  bgoldbtbndlem2  48304  bgoldbtbndlem3  48305  bgoldbtbnd  48307  dfnbgr6  48355  isuspgrimlem  48393  uhgrimisgrgric  48429  clnbgrgrim  48432  usgrgrtrirex  48448  isubgr3stgrlem4  48467  grilcbri2  48509  grlicsym  48511  grlictr  48513  gricgrlic  48516  gpgvtxedg0  48561  gpgvtxedg1  48562  gpgedg2ov  48564  gpgedg2iv  48565  pgnioedg1  48606  pgnioedg2  48607  pgnioedg3  48608  pgnioedg4  48609  pgnioedg5  48610  pgnbgreunbgrlem2lem3  48614  pgnbgreunbgrlem3  48616  pgnbgreunbgrlem5lem1  48618  pgnbgreunbgrlem5lem2  48619  pgnbgreunbgrlem5lem3  48620  pgnbgreunbgrlem6  48622  upgrwlkupwlk  48638  uspgrsprf1  48645  lmod0rng  48727  lidldomn1  48729  rngccatidALTV  48770  rngcinvALTV  48774  rhmsubcALTVlem4  48782  funcringcsetcALTV2lem9  48796  ringccatidALTV  48804  ringcbasbasALTV  48810  ztprmneprm  48845  pgrpgt2nabl  48864  lmodvsmdi  48877  ply1mulgsumlem2  48885  lincsumcl  48929  ellcoellss  48933  linindslinci  48946  islinindfis  48947  lincext3  48954  lindslinindimp2lem4  48959  lindslinindsimp2lem5  48960  lindslinindsimp2  48961  lindsrng01  48966  ldepspr  48971  lincresunit3lem1  48977  elfzolborelfzop1  49017  dignn0ldlem  49100  nn0sumshdiglem1  49119  1arymaptf1  49140  2arymaptf1  49151  rrx2xpref1o  49216  rrx2plord2  49220  rrx2plordisom  49221  line2ylem  49249  line2xlem  49251  line2y  49253  itschlc0xyqsol1  49264  inlinecirc02plem  49284  fullthinc  49947  tfis2d  50177  onsetrec  50205