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  1348  3expd  1353  mp3an1i  1455  minimp  1620  meredith  1640  19.35  1876  speimfw  1962  equtrr  2020  equeucl  2022  ax12ev2  2179  sbiedw  2315  cbv1v  2336  exsb  2360  cbv1  2405  ax12b  2427  axc11n  2429  dvelimdf  2452  equvel  2459  dfsb1  2484  sbied  2506  dfmoeu  2534  mo3  2562  mo4  2564  2mo  2646  2eu6  2655  exists2  2660  pm2.61dne  3017  rexlimdv  3140  r19.21v  3167  r19.12  3298  r19.12OLD  3299  2gencl  3508  3gencl  3509  vtocl2ga  3562  vtocl2gaf  3563  vtocl3gaf  3565  vtocl3ga  3567  vtocl4ga  3570  rspccv  3603  ceqex  3636  mob  3707  euind  3714  reuind  3743  2reu1  3879  sseq2  3992  nelss  4031  rexdifi  4132  reupick2  4313  disjeq0  4438  uneqdifeq  4475  sspw  4593  ssprsseq  4807  preq12b  4832  prnebg  4838  prel12g  4846  3elpr2eq  4888  iinss2  5039  trintss  5260  dtruALT2  5352  reusv2lem1  5380  alxfr  5389  ralxfrALT  5397  exexneq  5421  dtruOLD  5428  copsexgw  5477  copsexg  5478  snopeqop  5493  propeqop  5494  opthhausdorff  5504  opthhausdorff0  5505  pofun  5592  solin  5601  frss  5631  2optocl  5763  3optocl  5764  ssrel  5774  ssrelOLD  5775  ssrel2  5777  ssrelrel  5788  relop  5843  dfres3  5984  asymref2  6119  xpidtr  6124  trin2  6125  poltletr  6134  imadifssran  6153  xp11  6177  relcnvtrg  6268  reuop  6295  tz7.7  6391  ordtr2  6409  suc11  6472  iotavalOLD  6516  funmoOLD  6563  fundif  6596  fss  6733  f0dom0  6773  fv3  6905  tz6.12i  6915  mpteqb  7016  fveqdmss  7079  eldmrexrnb  7093  funopsn  7149  funsndifnop  7152  tpres  7204  funfvima  7233  fvclss  7244  f1veqaeq  7260  fvf1pr  7310  isoselem  7344  oprabv  7476  ovg  7581  elovmpt3rab1  7676  sorpsscmpl  7737  iunpw  7774  trom  7879  limom  7886  peano5  7898  focdmex  7963  funelss  8055  funeldmdif  8056  bropopvvv  8098  bropfvvvvlem  8099  f1o2ndf1  8130  poxp  8136  soxp  8137  poxp2  8151  frxp2  8152  frxp3  8159  suppimacnv  8182  ressuppss  8191  ressuppssdif  8193  tposfn2  8256  wfr3g  8330  onnseq  8367  smoel  8383  smogt  8390  smoiso2  8392  tfr3  8422  tz7.48-2  8465  tz7.48-3  8467  tz7.49  8468  oecl  8558  oaordex  8579  oalimcl  8581  oaass  8582  omordi  8587  omlimcl  8599  odi  8600  omeulem1  8603  oen0  8607  nnawordi  8642  nnaass  8643  nnmordi  8652  omabs  8672  omsmolem  8678  naddssim  8706  brinxper  8757  iiner  8812  2ecoptocl  8831  3ecoptocl  8832  undifixp  8957  xpdom2  9090  xpf1o  9162  infensuc  9178  findcard2  9187  php  9230  phpOLD  9242  onomeneqOLD  9249  isinf  9279  isinfOLD  9280  unblem2  9312  fodomfir  9351  infssuni  9369  finsschain  9382  fsuppunfi  9411  fsuppunbi  9412  marypha1  9457  hartogs  9567  card2on  9577  card2inf  9578  xpwdomg  9608  elirrv  9619  en3lp  9637  preleqg  9638  inf3lem1  9651  inf3lem2  9652  inf3lem3  9653  inf3lem5  9655  noinfep  9683  ttrclss  9743  ttrclselem2  9749  trcl  9751  tcel  9768  frr3g  9779  rankonidlem  9851  scottex  9908  djuunxp  9944  eldju2ndl  9947  updjud  9957  dif1card  10033  fodomnum  10080  cardaleph  10112  kmlem9  10182  kmlem13  10186  cflim2  10286  cfsmolem  10293  infpssrlem3  10328  isfin7-2  10419  fin1a2lem6  10428  fin1a2lem12  10434  domtriomlem  10465  axdc3lem4  10476  axdc4lem  10478  zorn2lem3  10521  zorn2lem4  10522  zorn2lem5  10523  zorn2lem7  10525  zornn0g  10528  axdclem2  10543  ondomon  10586  alephval2  10595  cfpwsdom  10607  wuncval2  10770  grupr  10820  gruiun  10822  ingru  10838  grothomex  10852  indpi  10930  nqereu  10952  prlem934  11056  reclem2pr  11071  mulgt0sr  11128  supsrlem  11134  dedekind  11407  lemul1a  12104  squeeze0  12154  peano5nni  12252  nnunb  12506  nn0lt2  12665  nn0le2is012  12666  fzind  12700  nn0ind-raph  12702  zindd  12703  eluzaddOLD  12896  uzin  12901  nn01to3  12966  xnn0xadd0  13272  xmulasslem  13310  icoshft  13496  fzen  13564  uzsubsubfz  13569  elfz0ubfz0  13655  elfz0fzfz0  13656  fz0fzelfz0  13657  elfzmlbp  13662  elfzodifsumelfzo  13753  ssfzo12bi  13783  fzoopth  13784  elfzonelfzo  13791  elfznelfzo  13794  injresinjlem  13809  injresinj  13810  modfzo0difsn  13967  modsumfzodifsn  13968  addmodlteq  13970  ssnn0fi  14009  fsuppmapnn0fiub0  14017  expcllem  14096  expeq0  14116  mulexp  14125  leexp2r  14197  bernneq  14251  facdiv  14309  hasheqf1oi  14373  hashnn0n0nn  14413  hashss  14431  hashgt12el  14444  hashgt12el2  14445  hashimarni  14463  hashle2pr  14499  pr2pwpr  14501  hashge2el2dif  14502  hashge2el2difr  14503  hashtpg  14507  hashge3el3dif  14509  exprelprel  14512  hash1to3  14514  hash3tpde  14515  tpfo  14522  fundmge2nop0  14524  fi1uzind  14529  ccatsymb  14603  swrdnd  14675  swrdnd2  14676  swrdnnn0nd  14677  swrdnd0  14678  pfxnd0  14709  swrdswrdlem  14725  swrdswrd  14726  pfxccatin12lem2a  14748  pfxccatin12lem1  14749  swrdccatin2  14750  pfxccatin12lem2  14752  pfxccatin12lem3  14753  pfxccat3  14755  swrdccat  14756  swrdccat3blem  14760  repsdf2  14799  repswswrd  14805  cshwidxmod  14824  cshwidx0  14827  cshf1  14831  cshweqrep  14842  cshw1  14843  cshwsexaOLD  14846  2cshwcshw  14847  scshwfzeqfzo  14848  cshwcsh2id  14850  wwlktovfo  14980  relexpaddg  15075  iseraltlem2  15702  modfsummods  15812  clim2prod  15907  prodfn0  15913  prodfrec  15914  prodmo  15955  fprodabs  15993  binomfallfac  16060  fprodefsum  16114  dvdsaddre2b  16327  addmodlteqALT  16345  oddge22np1  16369  nn0enne  16397  nn0o1gt2  16401  sumeven  16407  sumodd  16408  dvdslegcd  16524  gcdneg  16542  dfgcd2  16566  rplpwr  16578  lcmf  16653  lcmftp  16656  lcmfunsnlem2lem1  16658  lcmfunsnlem2  16660  lcmfdvdsb  16663  coprmdvds1  16672  qredeq  16677  coprmprod  16681  coprmproddvdslem  16682  cncongr1  16687  cncongr2  16688  prm2orodd  16711  2mulprm  16713  nnnn0modprm0  16827  prm23lt5  16835  prm23ge5  16836  dvdsprmpweqnn  16906  dvdsprmpweqle  16907  oddprmdvds  16924  prmpwdvds  16925  prmreclem4  16940  ramcl  17050  prmgaplem6  17077  prmgaplem7  17078  prmgaplem8  17079  cshwshashlem1  17116  cshwshashlem2  17117  cshwshashlem3  17118  cshwrepswhash1  17123  setsn0fun  17193  setsstruct2  17194  imasleval  17562  mreiincl  17615  mreexexd  17667  inveq  17794  cicsym  17824  cictr  17825  initoid  18022  termoid  18023  initoeu2lem0  18034  initoeu2lem1  18035  initoeu2lem2  18036  initoeu2  18037  fthestrcsetc  18170  fthsetcestrc  18185  drsdirfi  18326  isnmgm  18631  mgmhmlin  18686  issubmgm2  18690  sgrpass  18712  insubm  18805  mgm2nsgrplem3  18907  dfgrp3lem  19030  cyccom  19195  symg2bas  19383  symgfix2  19407  symgextf1  19412  gsmsymgrfix  19419  pmtrprfv3  19445  psgnunilem4  19488  efgi2  19716  0ringnnzr  20498  rnghmsscmap  20603  rnghmsubcsetclem2  20605  rngcinv  20610  funcrngcsetc  20613  funcrngcsetcALT  20614  rhmsscmap  20632  rhmsubcsetclem2  20634  rhmsubcrngclem2  20640  ringcbasbas  20646  funcringcsetc  20647  rhmsubclem4  20661  rngqiprngimfo  21278  psgndiflemB  21585  psgndiflemA  21586  elfrlmbasn0  21750  lmictra  21832  mpfrcl  22076  gsummoncoe1  22279  mamufacex  22367  matecl  22398  dmatelnd  22469  dmatscmcl  22476  scmateALT  22485  scmatsgrp1  22495  scmatf1  22504  mavmulsolcl  22524  cramerimplem1  22656  cramerimplem2  22657  pmatcollpw3fi1  22761  mp2pm2mplem4  22782  pm2mpfo  22787  chmaidscmat  22821  fvmptnn04ifb  22824  chfacfscmul0  22831  chfacfpmmul0  22835  cayhamlem1  22839  cayhamlem3  22860  cayleyhamilton1  22865  fiinopn  22874  tgcl  22942  distop  22968  isclo2  23061  iscldtop  23068  ssnei2  23089  opnnei  23093  pnfnei  23193  mnfnei  23194  tgcnp  23226  cnpnei  23237  1stcelcls  23434  txcnpi  23581  cnmptcom  23651  fbfinnfr  23814  isfildlem  23830  snfil  23837  fbunfip  23842  fgcl  23851  elfm2  23921  fmco  23934  fbflim2  23950  cnpflf2  23973  flimfcls  23999  tmdgsum  24068  neibl  24477  tngngpim  24635  fgcfil  25260  caubl  25297  volsuplem  25545  ellimc3  25869  dvnadd  25920  dvnres  25922  cpnord  25926  dvnfre  25945  ply1divex  26131  cxpmul2  26686  fsumdvdsmul  27193  zabsle1  27295  gausslemma2dlem1a  27364  gausslemma2dlem3  27367  lgsquad2lem2  27384  2lgs  27406  2sq2  27432  2sqnn0  27437  2sqnn  27438  2sqreultlem  27446  2sqreunnltlem  27449  qabvexp  27625  sltval2  27656  nolt02o  27695  ssltun1  27808  scutun12  27810  madebday  27893  mulsprop  28111  precsexlem8  28193  precsexlem9  28194  noseqind  28253  om2noseqrdg  28265  peano5uzs  28345  axcontlem4  28931  umgredgprv  29071  umgrnloop  29072  upgrpredgv  29103  upgredgpr  29106  edglnl  29107  usgredgprvALT  29159  usgrnloopALT  29167  usgredg2v  29191  fusgrfis  29294  nbuhgr2vtx1edgblem  29315  nb3grprlem1  29344  cusgrsize2inds  29418  cusgrfi  29423  fusgrn0degnn0  29464  uspgrloopvtxel  29481  vtxdginducedm1lem4  29507  uhgr0edg0rgrb  29539  wlkl1loop  29603  wlk1walk  29604  upgriswlk  29606  upgrwlkvtxedg  29610  uspgr2wlkeq  29611  wlkv0  29616  wlksoneq1eq2  29629  wlkon2n0  29631  wlkreslem  29634  wlkres  29635  lfgrwlkprop  29652  pthdivtx  29694  2pthnloop  29698  spthonepeq  29719  uhgrwkspthlem2  29721  uhgrwkspth  29722  usgr2wlkneq  29723  usgr2trlncl  29727  usgr2pthlem  29730  usgr2pth  29731  cyclnspth  29768  lfgrn1cycl  29772  usgr2trlncrct  29773  uspgrn2crct  29775  crctcshwlkn0lem3  29779  crctcshwlkn0lem5  29781  wwlknp  29810  wspthneq1eq2  29827  0enwwlksnge1  29831  wlklnwwlkln1  29835  wlkiswwlks2  29842  wlkiswwlksupgr2  29844  wlklnwwlkln2lem  29849  wwlksnred  29859  wwlksnextbi  29861  wwlksnredwwlkn0  29863  wwlksnextwrd  29864  wwlksnextinj  29866  wwlksnextproplem3  29878  wwlksnextprop  29879  wspthsnwspthsnon  29883  wspthsnonn0vne  29884  2pthon3v  29910  umgr2adedgwlkonALT  29914  umgr2wlk  29916  umgr2wlkon  29917  umgrwwlks2on  29924  elwspths2on  29927  usgr2wspthons3  29931  elwwlks2  29933  rusgrnumwwlk  29942  clwwlkccatlem  29955  clwlkclwwlklem2a4  29963  clwlkclwwlklem2a  29964  clwlkclwwlklem2  29966  clwlkclwwlkf1lem3  29972  erclwwlkeqlen  29985  clwwlknwwlksn  30004  loopclwwlkn1b  30008  clwwlkf1  30015  wwlksext2clwwlk  30023  eleclclwwlknlem2  30027  umgr2cwwk2dif  30030  eleclclwwlkn  30042  hashecclwwlkn1  30043  umgrhashecclwwlk  30044  clwwlknonwwlknonb  30072  clwwlknonex2lem2  30074  clwwlknonex2  30075  1pthon2v  30119  upgr3v3e3cycl  30146  uhgr3cyclexlem  30147  uhgr3cyclex  30148  eupth2lem3lem4  30197  frgr3vlem1  30239  frgr3vlem2  30240  3vfriswmgrlem  30243  3vfriswmgr  30244  3cyclfrgrrn1  30251  n4cyclfrgr  30257  frgrncvvdeqlem3  30267  frgrncvvdeqlem6  30270  frgrncvvdeqlem7  30271  frgrncvvdeqlem8  30272  frgrwopreglem4a  30276  frgrwopreglem3  30280  frgrwopreg1  30284  frgrwopreg2  30285  frgrwopreglem5lem  30286  frgrwopreglem5ALT  30288  frgrwopreg  30289  fusgr2wsp2nb  30300  2wspmdisj  30303  numclwwlk1lem2foa  30320  numclwwlk1lem2f1  30323  numclwwlk1lem2fo  30324  numclwwlk1  30327  wlkl0  30333  numclwwlk2lem1  30342  numclwlk2lem2f  30343  numclwlk2lem2f1o  30345  frgrreg  30360  frgrregord013  30361  frgrregord13  30362  friendshipgt3  30364  friendship  30365  eulplig  30451  ipassi  30807  ubthlem2  30837  isch3  31207  shintcli  31295  shmodsi  31355  spansncvi  31618  hoaddsub  31782  eigorthi  31803  pjss2coi  32130  pjnormssi  32134  pj3cor1i  32175  strb  32224  dmdmd  32266  mdsl0  32276  csmdsymi  32300  chrelat2i  32331  mdsymlem3  32371  mdsymlem6  32374  sumdmdlem2  32385  opreu2reuALT  32443  ssrelf  32574  gsumwun  33014  spthcycl  35075  loop1cycl  35083  cvmlift2lem1  35248  satfrel  35313  satfrnmapom  35316  fmlafvel  35331  fmla1  35333  gonarlem  35340  gonar  35341  goalrlem  35342  goalr  35343  satffunlem  35347  satffunlem1lem1  35348  satffunlem2lem1  35350  satffun  35355  satefvfmla1  35371  mrsubvrs  35468  mclsax  35515  3ccased  35660  dfon2lem3  35727  rdgprc  35736  cgrextend  35950  btwndiff  35969  btwnconn1lem12  36040  brsegle  36050  broutsideof2  36064  funray  36082  in-ax8  36166  ss-ax8  36167  elicc3  36259  nn0prpwlem  36264  nn0prpw  36265  fnessref  36299  neibastop2lem  36302  filnetlem4  36323  meran1  36353  waj-ax  36356  arg-ax  36358  bj-nnclavc  36490  bj-con2com  36503  bj-axdd2  36534  bj-alrimg  36561  bj-exlimg  36565  bj-exalimi  36575  bj-cbvalimt  36581  bj-eximcom  36585  bj-ssbid1ALT  36607  bj-sb  36629  bj-snsetex  36905  bj-restpw  37034  bj-finsumval0  37227  mptsnunlem  37280  icoreclin  37299  relowlpssretop  37306  inunissunidif  37317  rdgssun  37320  finorwe  37324  domalom  37346  wl-dral1d  37473  wl-exeq  37476  wl-lem-exsb  37508  poimirlem29  37597  poimirlem32  37600  fdc  37693  seqpo  37695  incsequz  37696  isismty  37749  ismtybndlem  37754  heibor1lem  37757  ismgmOLD  37798  isexid2  37803  ghomco  37839  pridlc  38019  relcnveq3  38263  elrelscnveq3  38433  cdleme18d  40238  tendovalco  40708  cdlemn11pre  41153  dihord2pre  41168  indstrd  42135  unitscyglem3  42139  nnadddir  42250  eu6w  42631  incssnn0  42667  fphpd  42772  jm2.19lem3  42948  setindtr  42981  islssfg2  43028  mpaaeu  43107  ordnexbtwnsuc  43225  oaabsb  43252  succlg  43286  oacl2g  43288  omabs2  43290  omcl2  43291  omcl3g  43292  pr2cv  43506  refimssco  43565  iunrelexpmin1  43666  iunrelexpmin2  43670  trclimalb2  43684  clsk1indlem3  44001  tfindsd  44169  mnurndlem1  44245  nzss  44281  sb5ALT  44490  truniALT  44506  ee223  44599  3orbi123VD  44815  sbc3orgVD  44816  exbirVD  44818  exbiriVD  44819  sbcim2gVD  44840  trsbcVD  44842  truniALTVD  44843  onfrALTlem3VD  44852  onfrALTlem2VD  44854  csbrngVD  44861  19.41rgVD  44867  ax6e2eqVD  44872  ax6e2ndeqVD  44874  2uasbanhVD  44876  sb5ALTVD  44878  vk15.4jVD  44879  infxrunb3rnmpt  45384  stoweidlem26  45986  et-equeucl  46832  hirstL-ax3  46850  rexsb  47057  rexrsb  47058  euoreqb  47067  2reu8i  47071  afvres  47130  tz6.12-afv  47131  afvco2  47134  afv2orxorb  47186  afv2res  47197  tz6.12-afv2  47198  tz6.12i-afv2  47201  dfatcolem  47213  zm1nn  47260  2ffzoeq  47285  smonoord  47304  iccpartiltu  47355  iccpartlt  47357  iccpartltu  47358  iccpartgtl  47359  iccpartgt  47360  iccpartleu  47361  iccpartgel  47362  icceuelpart  47369  iccpartnel  47371  lswn0  47377  ichnreuop  47405  ichreuopeq  47406  prsprel  47420  sprsymrelfvlem  47423  sprsymrelf1lem  47424  sprsymrelfolem2  47426  prproropf1olem4  47439  paireqne  47444  prprelb  47449  reupr  47455  goldbachth  47480  odz2prm2pw  47496  fmtno4prmfac  47505  fmtno4prmfac193  47506  prmdvdsfmtnof1lem2  47518  2pwp1prmfmtno  47523  lighneallem2  47539  lighneallem4b  47542  lighneallem4  47543  requad2  47556  odd2prm2  47651  mogoldbblem  47653  gbepos  47691  gbowgt5  47695  gbowge7  47696  stgoldbwt  47709  sbgoldbwt  47710  sbgoldbst  47711  sbgoldbaltlem1  47712  sbgoldbalt  47714  sbgoldbo  47720  nnsum3primesle9  47727  nnsum4primesodd  47729  nnsum4primesoddALTV  47730  nnsum4primeseven  47733  nnsum4primesevenALTV  47734  bgoldbtbndlem1  47738  bgoldbtbndlem2  47739  bgoldbtbndlem3  47740  bgoldbtbnd  47742  dfnbgr6  47789  isuspgrimlem  47820  uhgrimisgrgric  47845  clnbgrgrim  47848  usgrgrtrirex  47863  isubgr3stgrlem4  47882  grilcbri2  47917  grlicsym  47919  grlictr  47921  gricgrlic  47924  gpgvtxedg0  47967  gpgvtxedg1  47968  upgrwlkupwlk  48002  uspgrsprf1  48009  lmod0rng  48091  lidldomn1  48093  rngccatidALTV  48134  rngcinvALTV  48138  rhmsubcALTVlem4  48146  funcringcsetcALTV2lem9  48160  ringccatidALTV  48168  ringcbasbasALTV  48174  ztprmneprm  48209  pgrpgt2nabl  48228  lmodvsmdi  48241  ply1mulgsumlem2  48250  lincsumcl  48294  ellcoellss  48298  linindslinci  48311  islinindfis  48312  lincext3  48319  lindslinindimp2lem4  48324  lindslinindsimp2lem5  48325  lindslinindsimp2  48326  lindsrng01  48331  ldepspr  48336  lincresunit3lem1  48342  elfzolborelfzop1  48382  dignn0ldlem  48469  nn0sumshdiglem1  48488  1arymaptf1  48509  2arymaptf1  48520  rrx2xpref1o  48585  rrx2plord2  48589  rrx2plordisom  48590  line2ylem  48618  line2xlem  48620  line2y  48622  itschlc0xyqsol1  48633  inlinecirc02plem  48653  fullthinc  49065  tfis2d  49195  onsetrec  49223