Theorem com12 33

Description: Inference that swaps (commutes) antecedents in an implication. Inference associated with pm2.04 91. Its associated inference is mpi 21. (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 23	. 2 ⊢ (𝜓 → 𝜓)
2		com12.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5com 32	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  34  syl5  35  syl6com  38  mpcom  39  syli  40  syl2imc  42  pm2.27  43  syldc  49  pm2.43b  56  syl9r  79  com3r  88  pm2.86i  111  pm2.24  125  con3rr3  156  exptOLD  179  jad  189  pm2.61  194  syl5ibcom  248  syl5ibrcom  250  pm5.501  369  impcom  412  impd  415  expcom  418  expdcom  419  simplbi2com  507  imdistanri  579  syldbl2  854  jaod  872  orel1  901  pm2.62  912  pm2.75  946  pm2.64  956  ccased  1052  dedlem0b  1058  3impd  1365  3expd  1370  mp3an1i  1480  minimp  1648  meredith  1668  19.35  1904  speimfw  1990  equtrr  2049  equeucl  2051  ax12ev2  2222  sbiedw  2355  cbv1v  2374  exsb  2397  cbv1  2440  ax12b  2462  axc11n  2464  dvelimdf  2487  equvel  2494  dfsb1  2519  sbied  2541  dfmoeu  2569  mo3  2598  mo4  2600  2mo  2682  2eu6  2690  exists2  2695  pm2.61dne  3050  rexlimdv  3170  r19.21v  3196  r19.12  3320  2gencl  3505  3gencl  3506  vtocl2ga  3551  vtocl2gaf  3552  vtocl3gaf  3553  vtocl3ga  3554  vtocl4ga  3556  rspccv  3587  ceqex  3620  mob  3689  euind  3696  reuind  3725  2reu1  3859  sseq2  3971  nelss  4011  rexdifi  4112  reupick2  4292  disjeq0  4422  uneqdifeq  4458  sspw  4578  ssprsseq  4795  preq12b  4819  prnebg  4825  prel12g  4833  3elpr2eq  4875  iinss2  5026  trintss  5241  dtruALT2  5342  reusv2lem1  5370  alxfr  5379  ralxfrALT  5387  exexneq  5417  copsexgw  5473  copsexgwOLD  5474  copsexg  5475  snopeqop  5490  propeqop  5491  opthhausdorff  5501  opthhausdorff0  5502  pofun  5588  solin  5597  frss  5626  2optocl  5758  3optocl  5759  ssrel  5770  ssrel2  5772  ssrelrel  5783  relop  5837  dfres3  5984  asymref2  6118  xpidtr  6123  trin2  6124  poltletr  6133  xp11  6174  imadifssranOLD  6204  relcnvtrg  6269  reuop  6295  tz7.7  6387  ordtr2  6407  suc11  6471  fundif  6586  fss  6723  f0dom0  6763  fv3  6900  tz6.12i  6908  mpteqb  7010  fveqdmss  7074  eldmrexrnb  7088  funopsnOLD  7146  funsndifnop  7149  tpres  7200  funfvima  7229  fvclss  7240  f1veqaeq  7255  fvf1pr  7306  isoselem  7340  oprabv  7471  ovg  7576  elovmpt3rab1  7671  sorpsscmpl  7732  iunpw  7770  trom  7871  limom  7878  peano5  7890  focdmex  7953  funelss  8044  funeldmdif  8045  bropopvvv  8085  bropfvvvvlem  8086  f1o2ndf1  8117  poxp  8124  soxp  8125  poxp2  8139  frxp2  8140  frxp3  8147  suppimacnv  8170  ressuppss  8179  ressuppssdif  8181  tposfn2  8244  wfr3g  8316  onnseq  8331  smoel  8347  smogt  8354  smoiso2  8356  tfr3  8386  tz7.48-2  8429  tz7.48-3  8431  tz7.49  8432  oecl  8522  oaordex  8543  oalimcl  8545  oaass  8546  omordi  8551  omlimcl  8563  odi  8564  omeulem1  8567  oen0  8572  nnawordi  8607  nnaass  8608  nnmordi  8617  omabs  8637  omsmolem  8643  naddssim  8672  brinxper  8724  iiner  8787  2ecoptocl  8806  3ecoptocl  8807  undifixp  8932  xpdom2  9060  xpf1o  9127  infensuc  9143  findcard2  9149  php  9191  isinf  9225  unblem2  9253  fodomfir  9287  infssuni  9303  finsschain  9316  fsuppunfi  9348  fsuppunbi  9349  marypha1  9394  hartogs  9506  card2on  9516  card2inf  9517  xpwdomg  9547  elirrvOLD  9560  elirrvOLDOLD  9561  en3lp  9583  preleqg  9584  inf3lem1  9597  inf3lem2  9598  inf3lem3  9599  inf3lem5  9601  noinfep  9629  ttrclss  9689  ttrclselem2  9695  trcl  9697  tcel  9712  frr3g  9728  rankonidlem  9800  scottex  9859  djuunxp  9907  eldju2ndl  9910  updjud  9920  dif1card  9994  fodomnum  10041  cardaleph  10073  kmlem9  10142  kmlem13  10146  cflim2  10247  cfsmolem  10254  infpssrlem3  10289  isfin7-2  10380  fin1a2lem6  10389  fin1a2lem12  10395  domtriomlem  10426  axdc3lem4  10437  axdc4lem  10439  zorn2lem3  10482  zorn2lem4  10483  zorn2lem5  10484  zorn2lem7  10486  zornn0g  10489  axdclem2  10504  ondomon  10547  alephval2  10557  cfpwsdom  10569  wuncval2  10732  grupr  10782  gruiun  10784  ingru  10800  grothomex  10814  indpi  10892  nqereu  10914  prlem934  11018  reclem2pr  11033  mulgt0sr  11090  supsrlem  11096  1re  11208  dedekind  11373  lemul1a  12069  squeeze0  12118  peano5nni  12236  nnadddir  12292  nnunb  12500  nn0lt2  12659  nn0le2is012  12660  fzind  12694  nn0ind-raph  12696  zindd  12697  uzin  12898  nn01to3  12965  xnn0xadd0  13273  xmulasslem  13311  icoshft  13500  fzen  13569  uzsubsubfz  13574  elfz0ubfz0  13660  elfz0fzfz0  13661  fz0fzelfz0  13662  elfzmlbp  13667  elfzodifsumelfzo  13760  ssfzo12bi  13790  fzoopth  13791  elfzonelfzo  13798  elfznelfzo  13802  injresinjlem  13819  injresinj  13820  modfzo0difsn  13979  modsumfzodifsn  13980  addmodlteq  13982  ssnn0fi  14021  fsuppmapnn0fiub0  14029  expcllem  14108  expeq0  14128  mulexp  14137  leexp2r  14210  bernneq  14265  facdiv  14323  hasheqf1oi  14387  hashnn0n0nn  14427  hashss  14445  hashgt12el  14459  hashgt12el2  14460  hashimarni  14478  hashle2pr  14514  pr2pwpr  14516  hashge2el2dif  14517  hashge2el2difr  14518  hashtpg  14522  hashge3el3dif  14524  exprelprel  14527  hash1to3  14529  hash3tpde  14530  tpfo  14537  fundmge2nop0  14539  fi1uzind  14544  ccatsymb  14620  swrdnd  14692  swrdnd2  14693  swrdnnn0nd  14694  swrdnd0  14695  pfxnd0  14726  swrdswrdlem  14741  swrdswrd  14742  pfxccatin12lem2a  14764  pfxccatin12lem1  14765  swrdccatin2  14766  pfxccatin12lem2  14768  pfxccatin12lem3  14769  pfxccat3  14771  swrdccat  14772  swrdccat3blem  14776  repsdf2  14815  repswswrd  14821  cshwidxmod  14840  cshwidx0  14843  cshf1  14847  cshweqrep  14858  cshw1  14859  2cshwcshw  14862  scshwfzeqfzo  14863  cshwcsh2id  14865  wwlktovfo  14995  relexpaddg  15090  iseraltlem2  15734  modfsummods  15845  clim2prod  15942  prodfn0  15948  prodfrec  15949  prodmo  15990  fprodabs  16028  binomfallfac  16095  fprodefsum  16149  dvdsaddre2b  16365  addmodlteqALT  16383  oddge22np1  16407  nn0enne  16435  nn0o1gt2  16439  sumeven  16445  sumodd  16446  dvdslegcd  16562  gcdneg  16580  dfgcd2  16604  rplpwr  16616  lcmf  16691  lcmftp  16694  lcmfunsnlem2lem1  16696  lcmfunsnlem2  16698  lcmfdvdsb  16701  coprmdvds1  16710  qredeq  16715  coprmprod  16719  coprmproddvdslem  16720  cncongr1  16725  cncongr2  16726  prm2orodd  16749  2mulprm  16751  nnnn0modprm0  16866  prm23lt5  16874  prm23ge5  16875  dvdsprmpweqnn  16945  dvdsprmpweqle  16946  oddprmdvds  16963  prmpwdvds  16964  prmreclem4  16979  ramcl  17089  prmgaplem6  17116  prmgaplem7  17117  prmgaplem8  17118  cshwshashlem1  17155  cshwshashlem2  17156  cshwshashlem3  17157  cshwrepswhash1  17162  setsn0fun  17233  setsstruct2  17234  imasleval  17595  mreiincl  17648  mreexexd  17704  inveq  17831  cicsym  17861  cictr  17862  initoid  18058  termoid  18059  initoeu2lem0  18070  initoeu2lem1  18071  initoeu2lem2  18072  initoeu2  18073  fthestrcsetc  18206  fthsetcestrc  18221  drsdirfi  18361  isnmgm  18702  mgmhmlin  18757  issubmgm2  18761  sgrpass  18783  insubm  18877  mgm2nsgrplem3  18982  dfgrp3lem  19104  cyccom  19274  symg2bas  19463  symgfix2  19486  symgextf1  19491  gsmsymgrfix  19498  pmtrprfv3  19524  psgnunilem4  19567  efgi2  19795  0ringnnzr  20609  rnghmsscmap  20715  rnghmsubcsetclem2  20717  rngcinv  20722  funcrngcsetc  20725  funcrngcsetcALT  20726  rhmsscmap  20744  rhmsubcsetclem2  20746  rhmsubcrngclem2  20752  ringcbasbas  20758  funcringcsetc  20759  rhmsubclem4  20773  unichnlidl  21340  rngqiprngimfo  21412  psgndiflemB  21719  psgndiflemA  21720  elfrlmbasn0  21882  lmictra  21964  mpfrcl  22205  gsummoncoe1  22437  mamufacex  22522  matecl  22551  dmatelnd  22622  dmatscmcl  22629  scmateALT  22638  scmatsgrp1  22648  scmatf1  22657  mavmulsolcl  22677  cramerimplem1  22809  cramerimplem2  22810  pmatcollpw3fi1  22914  mp2pm2mplem4  22935  pm2mpfo  22940  chmaidscmat  22974  fvmptnn04ifb  22977  chfacfscmul0  22984  chfacfpmmul0  22988  cayhamlem1  22992  cayhamlem3  23013  cayleyhamilton1  23018  fiinopn  23027  tgcl  23095  distop  23121  isclo2  23214  iscldtop  23221  ssnei2  23242  opnnei  23246  pnfnei  23346  mnfnei  23347  tgcnp  23379  cnpnei  23390  1stcelcls  23587  txcnpi  23734  cnmptcom  23804  fbfinnfr  23967  isfildlem  23983  snfil  23990  fbunfip  23995  fgcl  24004  elfm2  24074  fmco  24087  fbflim2  24103  cnpflf2  24126  flimfcls  24152  tmdgsum  24221  neibl  24627  tngngpim  24785  fgcfil  25399  caubl  25436  volsuplem  25683  ellimc3  26007  dvnadd  26057  dvnres  26059  cpnord  26063  dvnfre  26080  ply1divex  26263  cxpmul2  26820  fsumdvdsmul  27325  zabsle1  27426  gausslemma2dlem1a  27495  gausslemma2dlem3  27498  lgsquad2lem2  27515  2lgs  27537  2sq2  27563  2sqnn0  27568  2sqnn  27569  2sqreultlem  27577  2sqreunnltlem  27580  qabvexp  27756  ltsval2  27786  nolt02o  27825  sltsun1  27947  cutsun12  27949  madebday  28059  mulsprop  28289  precsexlem8  28373  precsexlem9  28374  noseqind  28451  om2noseqrdg  28463  n0cutlt  28518  peano5uzs  28563  expadds  28594  bdaypw2n0bndlem  28622  bdaypw2n0bnd  28623  axcontlem4  29258  umgredgprv  29398  umgrnloop  29399  upgrpredgv  29430  upgredgpr  29433  edglnl  29434  usgredgprvALT  29486  usgrnloopALT  29494  usgredg2v  29518  fusgrfis  29621  nbuhgr2vtx1edgblem  29642  nb3grprlem1  29671  cusgrsize2inds  29744  cusgrfi  29749  fusgrn0degnn0  29790  uspgrloopvtxel  29807  vtxdginducedm1lem4  29833  uhgr0edg0rgrb  29865  wlkl1loop  29928  wlk1walk  29929  upgriswlk  29931  upgrwlkvtxedg  29935  uspgr2wlkeq  29936  wlkv0  29940  wlksoneq1eq2  29953  wlkon2n0  29955  wlkreslem  29958  wlkres  29959  lfgrwlkprop  29976  pthdivtx  30017  2pthnloop  30021  spthonepeq  30042  uhgrwkspthlem2  30044  uhgrwkspth  30045  usgr2wlkneq  30046  usgr2trlncl  30050  usgr2pthlem  30053  usgr2pth  30054  cyclnspth  30091  lfgrn1cycl  30095  usgr2trlncrct  30096  uspgrn2crct  30098  crctcshwlkn0lem3  30102  crctcshwlkn0lem5  30104  wwlknp  30133  wspthneq1eq2  30150  0enwwlksnge1  30154  wlklnwwlkln1  30158  wlkiswwlks2  30165  wlkiswwlksupgr2  30167  wlklnwwlkln2lem  30172  wwlksnred  30182  wwlksnextbi  30184  wwlksnredwwlkn0  30186  wwlksnextwrd  30187  wwlksnextinj  30189  wwlksnextproplem3  30201  wwlksnextprop  30202  wspthsnwspthsnon  30206  wspthsnonn0vne  30207  2pthon3v  30233  umgr2adedgwlkonALT  30237  umgr2wlk  30239  umgr2wlkon  30240  usgrwwlks2on  30248  umgrwwlks2on  30249  elwspths2on  30252  elwspths2onw  30253  usgr2wspthons3  30257  elwwlks2  30259  rusgrnumwwlk  30268  clwwlkccatlem  30281  clwlkclwwlklem2a4  30289  clwlkclwwlklem2a  30290  clwlkclwwlklem2  30292  clwlkclwwlkf1lem3  30298  erclwwlkeqlen  30311  clwwlknwwlksn  30330  loopclwwlkn1b  30334  clwwlkf1  30341  wwlksext2clwwlk  30349  eleclclwwlknlem2  30353  umgr2cwwk2dif  30356  eleclclwwlkn  30368  hashecclwwlkn1  30369  umgrhashecclwwlk  30370  clwwlknonwwlknonb  30398  clwwlknonex2lem2  30400  clwwlknonex2  30401  1pthon2v  30445  upgr3v3e3cycl  30472  uhgr3cyclexlem  30473  uhgr3cyclex  30474  eupth2lem3lem4  30523  frgr3vlem1  30565  frgr3vlem2  30566  3vfriswmgrlem  30569  3vfriswmgr  30570  3cyclfrgrrn1  30577  n4cyclfrgr  30583  frgrncvvdeqlem3  30593  frgrncvvdeqlem6  30596  frgrncvvdeqlem7  30597  frgrncvvdeqlem8  30598  frgrwopreglem4a  30602  frgrwopreglem3  30606  frgrwopreg1  30610  frgrwopreg2  30611  frgrwopreglem5lem  30612  frgrwopreglem5ALT  30614  frgrwopreg  30615  fusgr2wsp2nb  30626  2wspmdisj  30629  numclwwlk1lem2foa  30646  numclwwlk1lem2f1  30649  numclwwlk1lem2fo  30650  numclwwlk1  30653  wlkl0  30659  numclwwlk2lem1  30668  numclwlk2lem2f  30669  numclwlk2lem2f1o  30671  frgrreg  30686  frgrregord013  30687  frgrregord13  30688  friendshipgt3  30690  friendship  30691  eulplig  30778  ipassi  31134  ubthlem2  31164  isch3  31534  shintcli  31622  shmodsi  31682  spansncvi  31945  hoaddsub  32109  eigorthi  32130  pjss2coi  32457  pjnormssi  32461  pj3cor1i  32502  strb  32551  dmdmd  32593  mdsl0  32603  csmdsymi  32627  chrelat2i  32658  mdsymlem3  32698  mdsymlem6  32701  sumdmdlem2  32712  opreu2reuALT  32764  ssrelf  32901  gsumwun  33337  r1filim  35440  trssfir1om  35447  fineqvinfep  35461  trssfir1omregs  35472  onvf1odlem4  35489  spthcycl  35520  loop1cycl  35528  cvmlift2lem1  35693  satfrel  35758  satfrnmapom  35761  fmlafvel  35776  fmla1  35778  gonarlem  35785  gonar  35786  goalrlem  35787  goalr  35788  satffunlem  35792  satffunlem1lem1  35793  satffunlem2lem1  35795  satffun  35800  satefvfmla1  35816  mrsubvrs  35913  mclsax  35960  3ccased  36110  dfon2lem3  36174  rdgprc  36183  cgrextend  36399  btwndiff  36418  btwnconn1lem12  36489  brsegle  36499  broutsideof2  36513  funray  36531  in-ax8  36625  ss-ax8  36626  elicc3  36717  nn0prpwlem  36722  nn0prpw  36723  fnessref  36757  neibastop2lem  36760  filnetlem4  36781  meran1  36811  waj-ax  36814  arg-ax  36816  axtco1from2  36875  dfttc4  36930  mh-inf3f1  36941  mh-regprimbi  36945  bj-nnclavc  37025  bj-con2com  37042  bj-axdd2  37074  bj-alrimg  37095  bj-exlimg  37117  bj-exalimi  37127  bj-eximcom  37128  bj-ssbid1ALT  37176  bj-sb  37201  bj-snsetex  37487  bj-axseprep  37599  bj-axreprepsep  37600  bj-restpw  37622  bj-finsumval0  37817  mptsnunlem  37872  icoreclin  37891  relowlpssretop  37898  inunissunidif  37909  rdgssun  37912  finorwe  37916  domalom  37938  wl-dral1d  38074  wl-exeq  38077  wl-lem-exsb  38109  wl-eujustlem1  38131  poimirlem29  38188  poimirlem32  38191  fdc  38284  seqpo  38286  incsequz  38287  isismty  38340  ismtybndlem  38345  heibor1lem  38348  ismgmOLD  38389  isexid2  38394  ghomco  38430  pridlc  38610  relcnveq3  38866  elrelscnveq3  39166  cdleme18d  40959  tendovalco  41429  cdlemn11pre  41874  dihord2pre  41889  indstrd  42850  unitscyglem3  42854  eu6w  43300  incssnn0  43334  fphpd  43435  jm2.19lem3  43610  setindtr  43643  islssfg2  43690  mpaaeu  43769  ordnexbtwnsuc  43886  oaabsb  43913  succlg  43947  oacl2g  43949  omabs2  43951  omcl2  43952  omcl3g  43953  pr2cv  44166  refimssco  44225  iunrelexpmin1  44326  iunrelexpmin2  44330  trclimalb2  44344  clsk1indlem3  44661  tfindsd  44826  mnurndlem1  44883  nzss  44919  sb5ALT  45126  truniALT  45142  ee223  45235  3orbi123VD  45450  sbc3orgVD  45451  exbirVD  45453  exbiriVD  45454  sbcim2gVD  45475  trsbcVD  45477  truniALTVD  45478  onfrALTlem3VD  45487  onfrALTlem2VD  45489  csbrngVD  45496  19.41rgVD  45502  ax6e2eqVD  45507  ax6e2ndeqVD  45509  2uasbanhVD  45511  sb5ALTVD  45513  vk15.4jVD  45514  infxrunb3rnmpt  46034  stoweidlem26  46632  et-equeucl  47478  hirstL-ax3  47518  rexsb  47725  rexrsb  47726  euoreqb  47735  2reu8i  47739  afvres  47798  tz6.12-afv  47799  afvco2  47802  afv2orxorb  47854  afv2res  47865  tz6.12-afv2  47866  tz6.12i-afv2  47869  dfatcolem  47881  zm1nn  47928  2ffzoeq  47954  smonoord  48003  iccpartiltu  48060  iccpartlt  48062  iccpartltu  48063  iccpartgtl  48064  iccpartgt  48065  iccpartleu  48066  iccpartgel  48067  icceuelpart  48074  iccpartnel  48076  lswn0  48082  ichnreuop  48110  ichreuopeq  48111  prsprel  48125  sprsymrelfvlem  48128  sprsymrelf1lem  48129  sprsymrelfolem2  48131  prproropf1olem4  48144  paireqne  48149  prprelb  48154  reupr  48160  goldbachth  48188  odz2prm2pw  48204  fmtno4prmfac  48213  fmtno4prmfac193  48214  prmdvdsfmtnof1lem2  48226  2pwp1prmfmtno  48231  lighneallem2  48247  lighneallem4b  48250  lighneallem4  48251  requad2  48277  odd2prm2  48372  mogoldbblem  48374  gbepos  48412  gbowgt5  48416  gbowge7  48417  stgoldbwt  48430  sbgoldbwt  48431  sbgoldbst  48432  sbgoldbaltlem1  48433  sbgoldbalt  48435  sbgoldbo  48441  nnsum3primesle9  48448  nnsum4primesodd  48450  nnsum4primesoddALTV  48451  nnsum4primeseven  48454  nnsum4primesevenALTV  48455  bgoldbtbndlem1  48459  bgoldbtbndlem2  48460  bgoldbtbndlem3  48461  bgoldbtbnd  48463  dfnbgr6  48511  isuspgrimlem  48549  uhgrimisgrgric  48585  clnbgrgrim  48588  usgrgrtrirex  48604  isubgr3stgrlem4  48623  grilcbri2  48665  grlicsym  48667  grlictr  48669  gricgrlic  48672  gpgvtxedg0  48717  gpgvtxedg1  48718  gpgedg2ov  48720  gpgedg2iv  48721  pgnioedg1  48762  pgnioedg2  48763  pgnioedg3  48764  pgnioedg4  48765  pgnioedg5  48766  pgnbgreunbgrlem2lem3  48770  pgnbgreunbgrlem3  48772  pgnbgreunbgrlem5lem1  48774  pgnbgreunbgrlem5lem2  48775  pgnbgreunbgrlem5lem3  48776  pgnbgreunbgrlem6  48778  upgrwlkupwlk  48794  uspgrsprf1  48801  lmod0rng  48883  lidldomn1  48885  rngccatidALTV  48926  rngcinvALTV  48930  rhmsubcALTVlem4  48938  funcringcsetcALTV2lem9  48952  ringccatidALTV  48960  ringcbasbasALTV  48966  ztprmneprm  49012  pgrpgt2nabl  49031  lmodvsmdi  49044  ply1mulgsumlem2  49052  lincsumcl  49096  ellcoellss  49100  linindslinci  49113  islinindfis  49114  lincext3  49121  lindslinindimp2lem4  49126  lindslinindsimp2lem5  49127  lindslinindsimp2  49128  lindsrng01  49133  ldepspr  49138  lincresunit3lem1  49144  elfzolborelfzop1  49184  dignn0ldlem  49267  nn0sumshdiglem1  49286  1arymaptf1  49307  2arymaptf1  49318  rrx2xpref1o  49383  rrx2plord2  49387  rrx2plordisom  49388  line2ylem  49416  line2xlem  49418  line2y  49420  itschlc0xyqsol1  49431  inlinecirc02plem  49451  fullthinc  50113  tfis2d  50343  onsetrec  50371