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  191  syl5ibcom  244  syl5ibrcom  246  pm5.501  367  impcom  409  impd  412  expcom  415  expdcom  416  simplbi2com  504  imdistanri  571  syldbl2  840  jaod  858  orel1  888  pm2.62  899  pm2.75  933  pm2.64  941  ccased  1038  dedlem0b  1044  3impd  1349  3expd  1354  mp3an1i  1455  minimp  1624  meredith  1644  19.35  1881  speimfw  1968  equtrr  2026  equeucl  2028  sbiedw  2310  cbv1v  2333  exsb  2356  cbv1  2402  ax12b  2424  axc11n  2426  dvelimdf  2449  equvel  2456  dfsb1  2481  sbied  2503  dfmoeu  2531  mo3  2559  mo4  2561  2mo  2645  2eu6  2653  exists2  2658  pm2.61dne  3029  rexlimdv  3154  r19.21v  3180  r19.12  3312  r19.12OLD  3313  2gencl  3517  3gencl  3518  vtocl2ga  3567  rspccv  3610  ceqex  3641  mob  3714  euind  3721  reuind  3750  2reu1  3892  sseq2  4009  nelss  4048  rexdifi  4146  reupick2  4321  rspn0OLD  4354  disjeq0  4456  uneqdifeq  4493  sspw  4614  ssprsseq  4829  preq12b  4852  prnebg  4857  prel12g  4865  3elpr2eq  4908  iinss2  5061  trintss  5285  dtruALT2  5369  reusv2lem1  5397  alxfr  5406  ralxfrALT  5414  exexneq  5435  dtruOLD  5442  copsexgw  5491  copsexg  5492  snopeqop  5507  propeqop  5508  opthhausdorff  5518  opthhausdorff0  5519  poclOLD  5597  pofun  5607  solin  5614  frss  5644  2optocl  5772  3optocl  5773  ssrel  5783  ssrelOLD  5784  ssrel2  5786  ssrelrel  5797  relop  5851  dfres3  5987  asymref2  6119  xpidtr  6124  trin2  6125  poltletr  6134  xp11  6175  relcnvtrg  6266  reuop  6293  tz7.7  6391  ordtr2  6409  suc11  6472  iotavalOLD  6518  funmoOLD  6565  fundif  6598  fss  6735  f0dom0  6776  fv3  6910  tz6.12i  6920  mpteqb  7018  fveqdmss  7081  eldmrexrnb  7094  funopsn  7146  funsndifnop  7149  tpres  7202  funfvima  7232  fvclss  7241  f1veqaeq  7256  isoselem  7338  oprabv  7469  ovg  7572  elovmpt3rab1  7666  sorpsscmpl  7724  iunpw  7758  trom  7864  limom  7871  peano5  7884  peano5OLD  7885  focdmex  7942  funelss  8033  funeldmdif  8034  bropopvvv  8076  bropfvvvvlem  8077  f1o2ndf1  8108  poxp  8114  soxp  8115  poxp2  8129  frxp2  8130  frxp3  8137  suppimacnv  8159  ressuppss  8168  ressuppssdif  8170  tposfn2  8233  wfr3g  8307  onnseq  8344  smoel  8360  smogt  8367  smoiso2  8369  tfr3  8399  tz7.48-2  8442  tz7.48-3  8444  tz7.49  8445  oecl  8537  oaordex  8558  oalimcl  8560  oaass  8561  omordi  8566  omlimcl  8578  odi  8579  omeulem1  8582  oen0  8586  nnawordi  8621  nnaass  8622  nnmordi  8631  omabs  8650  omsmolem  8656  naddssim  8684  iiner  8783  2ecoptocl  8802  3ecoptocl  8803  undifixp  8928  xpdom2  9067  xpf1o  9139  infensuc  9155  findcard2  9164  php  9210  phpOLD  9222  onomeneqOLD  9229  isinf  9260  isinfOLD  9261  findcard2OLD  9284  unblem2  9296  infssuni  9343  finsschain  9359  fsuppunfi  9383  fsuppunbi  9384  marypha1  9429  hartogs  9539  card2on  9549  card2inf  9550  xpwdomg  9580  elirrv  9591  en3lp  9609  preleqg  9610  inf3lem1  9623  inf3lem2  9624  inf3lem3  9625  inf3lem5  9627  noinfep  9655  ttrclss  9715  ttrclselem2  9721  trcl  9723  tcel  9740  frr3g  9751  rankonidlem  9823  scottex  9880  djuunxp  9916  eldju2ndl  9919  updjud  9929  dif1card  10005  fodomnum  10052  cardaleph  10084  kmlem9  10153  kmlem13  10157  cflim2  10258  cfsmolem  10265  infpssrlem3  10300  isfin7-2  10391  fin1a2lem6  10400  fin1a2lem12  10406  domtriomlem  10437  axdc3lem4  10448  axdc4lem  10450  zorn2lem3  10493  zorn2lem4  10494  zorn2lem5  10495  zorn2lem7  10497  zornn0g  10500  axdclem2  10515  ondomon  10558  alephval2  10567  cfpwsdom  10579  wuncval2  10742  grupr  10792  gruiun  10794  ingru  10810  grothomex  10824  indpi  10902  nqereu  10924  prlem934  11028  reclem2pr  11043  mulgt0sr  11100  supsrlem  11106  dedekind  11377  lemul1a  12068  squeeze0  12117  peano5nni  12215  nnunb  12468  nn0lt2  12625  nn0le2is012  12626  fzind  12660  nn0ind-raph  12662  zindd  12663  eluzaddOLD  12857  uzin  12862  nn01to3  12925  xnn0xadd0  13226  xmulasslem  13264  icoshft  13450  fzen  13518  uzsubsubfz  13523  elfz0ubfz0  13605  elfz0fzfz0  13606  fz0fzelfz0  13607  elfzmlbp  13612  elfzodifsumelfzo  13698  ssfzo12bi  13727  elfzonelfzo  13734  elfznelfzo  13737  injresinjlem  13752  injresinj  13753  modfzo0difsn  13908  modsumfzodifsn  13909  addmodlteq  13911  ssnn0fi  13950  fsuppmapnn0fiub0  13958  expcllem  14038  expeq0  14058  mulexp  14067  leexp2r  14139  bernneq  14192  facdiv  14247  hasheqf1oi  14311  hashnn0n0nn  14351  hashss  14369  hashgt12el  14382  hashgt12el2  14383  hashimarni  14401  hashle2pr  14438  pr2pwpr  14440  hashge2el2dif  14441  hashge2el2difr  14442  hashtpg  14446  hashge3el3dif  14447  exprelprel  14450  hash1to3  14452  fundmge2nop0  14453  fi1uzind  14458  ccatsymb  14532  swrdnd  14604  swrdnd2  14605  swrdnnn0nd  14606  swrdnd0  14607  pfxnd0  14638  swrdswrdlem  14654  swrdswrd  14655  pfxccatin12lem2a  14677  pfxccatin12lem1  14678  swrdccatin2  14679  pfxccatin12lem2  14681  pfxccatin12lem3  14682  pfxccat3  14684  swrdccat  14685  swrdccat3blem  14689  repsdf2  14728  repswswrd  14734  cshwidxmod  14753  cshwidx0  14756  cshf1  14760  cshweqrep  14771  cshw1  14772  cshwsexaOLD  14775  2cshwcshw  14776  scshwfzeqfzo  14777  cshwcsh2id  14779  wwlktovfo  14909  relexpaddg  15000  iseraltlem2  15629  modfsummods  15739  clim2prod  15834  prodfn0  15840  prodfrec  15841  prodmo  15880  fprodabs  15918  binomfallfac  15985  fprodefsum  16038  dvdsaddre2b  16250  addmodlteqALT  16268  oddge22np1  16292  nn0enne  16320  nn0o1gt2  16324  sumeven  16330  sumodd  16331  dvdslegcd  16445  gcdneg  16463  dfgcd2  16488  rplpwr  16499  lcmf  16570  lcmftp  16573  lcmfunsnlem2lem1  16575  lcmfunsnlem2  16577  lcmfdvdsb  16580  coprmdvds1  16589  qredeq  16594  coprmprod  16598  coprmproddvdslem  16599  cncongr1  16604  cncongr2  16605  prm2orodd  16628  2mulprm  16630  nnnn0modprm0  16739  prm23lt5  16747  prm23ge5  16748  dvdsprmpweqnn  16818  dvdsprmpweqle  16819  oddprmdvds  16836  prmpwdvds  16837  prmreclem4  16852  ramcl  16962  prmgaplem6  16989  prmgaplem7  16990  prmgaplem8  16991  cshwshashlem1  17029  cshwshashlem2  17030  cshwshashlem3  17031  cshwrepswhash1  17036  setsn0fun  17106  setsstruct2  17107  imasleval  17487  mreiincl  17540  mreexexd  17592  inveq  17721  cicsym  17751  cictr  17752  initoid  17951  termoid  17952  initoeu2lem0  17963  initoeu2lem1  17964  initoeu2lem2  17965  initoeu2  17966  fthestrcsetc  18102  fthsetcestrc  18117  drsdirfi  18258  isnmgm  18565  sgrpass  18616  insubm  18699  mgm2nsgrplem3  18801  dfgrp3lem  18921  cyccom  19080  symg2bas  19260  symgfix2  19284  symgextf1  19289  gsmsymgrfix  19296  pmtrprfv3  19322  psgnunilem4  19365  efgi2  19593  0ringnnzr  20302  psgndiflemB  21153  psgndiflemA  21154  elfrlmbasn0  21318  lmictra  21400  mpfrcl  21648  gsummoncoe1  21828  mamufacex  21891  matecl  21927  dmatelnd  21998  dmatscmcl  22005  scmateALT  22014  scmatsgrp1  22024  scmatf1  22033  mavmulsolcl  22053  cramerimplem1  22185  cramerimplem2  22186  pmatcollpw3fi1  22290  mp2pm2mplem4  22311  pm2mpfo  22316  chmaidscmat  22350  fvmptnn04ifb  22353  chfacfscmul0  22360  chfacfpmmul0  22364  cayhamlem1  22368  cayhamlem3  22389  cayleyhamilton1  22394  fiinopn  22403  tgcl  22472  distop  22498  isclo2  22592  iscldtop  22599  ssnei2  22620  opnnei  22624  pnfnei  22724  mnfnei  22725  tgcnp  22757  cnpnei  22768  1stcelcls  22965  txcnpi  23112  cnmptcom  23182  fbfinnfr  23345  isfildlem  23361  snfil  23368  fbunfip  23373  fgcl  23382  elfm2  23452  fmco  23465  fbflim2  23481  cnpflf2  23504  flimfcls  23530  tmdgsum  23599  neibl  24010  tngngpim  24176  fgcfil  24788  caubl  24825  volsuplem  25072  ellimc3  25396  dvnadd  25446  dvnres  25448  cpnord  25452  dvnfre  25469  ply1divex  25654  cxpmul2  26197  zabsle1  26799  gausslemma2dlem1a  26868  gausslemma2dlem3  26871  lgsquad2lem2  26888  2lgs  26910  2sq2  26936  2sqnn0  26941  2sqnn  26942  2sqreultlem  26950  2sqreunnltlem  26953  qabvexp  27129  sltval2  27159  nolt02o  27198  ssltun1  27309  scutun12  27311  madebday  27394  mulsprop  27586  precsexlem8  27660  precsexlem9  27661  axcontlem4  28225  umgredgprv  28367  umgrnloop  28368  upgrpredgv  28399  upgredgpr  28402  edglnl  28403  usgredgprvALT  28452  usgrnloopALT  28460  usgredg2v  28484  fusgrfis  28587  nbuhgr2vtx1edgblem  28608  nb3grprlem1  28637  cusgrsize2inds  28710  cusgrfi  28715  fusgrn0degnn0  28756  uspgrloopvtxel  28773  vtxdginducedm1lem4  28799  uhgr0edg0rgrb  28831  wlkl1loop  28895  wlk1walk  28896  upgriswlk  28898  upgrwlkvtxedg  28902  uspgr2wlkeq  28903  wlkv0  28908  wlksoneq1eq2  28921  wlkon2n0  28923  wlkreslem  28926  wlkres  28927  lfgrwlkprop  28944  pthdivtx  28986  2pthnloop  28988  spthonepeq  29009  uhgrwkspthlem2  29011  uhgrwkspth  29012  usgr2wlkneq  29013  usgr2trlncl  29017  usgr2pthlem  29020  usgr2pth  29021  cyclnspth  29057  lfgrn1cycl  29059  usgr2trlncrct  29060  uspgrn2crct  29062  crctcshwlkn0lem3  29066  crctcshwlkn0lem5  29068  wwlknp  29097  wspthneq1eq2  29114  0enwwlksnge1  29118  wlklnwwlkln1  29122  wlkiswwlks2  29129  wlkiswwlksupgr2  29131  wlklnwwlkln2lem  29136  wwlksnred  29146  wwlksnextbi  29148  wwlksnredwwlkn0  29150  wwlksnextwrd  29151  wwlksnextinj  29153  wwlksnextproplem3  29165  wwlksnextprop  29166  wspthsnwspthsnon  29170  wspthsnonn0vne  29171  2pthon3v  29197  umgr2adedgwlkonALT  29201  umgr2wlk  29203  umgr2wlkon  29204  umgrwwlks2on  29211  elwspths2on  29214  usgr2wspthons3  29218  elwwlks2  29220  rusgrnumwwlk  29229  clwwlkccatlem  29242  clwlkclwwlklem2a4  29250  clwlkclwwlklem2a  29251  clwlkclwwlklem2  29253  clwlkclwwlkf1lem3  29259  erclwwlkeqlen  29272  clwwlknwwlksn  29291  loopclwwlkn1b  29295  clwwlkf1  29302  wwlksext2clwwlk  29310  eleclclwwlknlem2  29314  umgr2cwwk2dif  29317  eleclclwwlkn  29329  hashecclwwlkn1  29330  umgrhashecclwwlk  29331  clwwlknonwwlknonb  29359  clwwlknonex2lem2  29361  clwwlknonex2  29362  1pthon2v  29406  upgr3v3e3cycl  29433  uhgr3cyclexlem  29434  uhgr3cyclex  29435  eupth2lem3lem4  29484  frgr3vlem1  29526  frgr3vlem2  29527  3vfriswmgrlem  29530  3vfriswmgr  29531  3cyclfrgrrn1  29538  n4cyclfrgr  29544  frgrncvvdeqlem3  29554  frgrncvvdeqlem6  29557  frgrncvvdeqlem7  29558  frgrncvvdeqlem8  29559  frgrwopreglem4a  29563  frgrwopreglem3  29567  frgrwopreg1  29571  frgrwopreg2  29572  frgrwopreglem5lem  29573  frgrwopreglem5ALT  29575  frgrwopreg  29576  fusgr2wsp2nb  29587  2wspmdisj  29590  numclwwlk1lem2foa  29607  numclwwlk1lem2f1  29610  numclwwlk1lem2fo  29611  numclwwlk1  29614  wlkl0  29620  numclwwlk2lem1  29629  numclwlk2lem2f  29630  numclwlk2lem2f1o  29632  frgrreg  29647  frgrregord013  29648  frgrregord13  29649  friendshipgt3  29651  friendship  29652  eulplig  29738  ipassi  30094  ubthlem2  30124  isch3  30494  shintcli  30582  shmodsi  30642  spansncvi  30905  hoaddsub  31069  eigorthi  31090  pjss2coi  31417  pjnormssi  31421  pj3cor1i  31462  strb  31511  dmdmd  31553  mdsl0  31563  csmdsymi  31587  chrelat2i  31618  mdsymlem3  31658  mdsymlem6  31661  sumdmdlem2  31672  opreu2reuALT  31717  ssrelf  31844  spthcycl  34120  loop1cycl  34128  cvmlift2lem1  34293  satfrel  34358  satfrnmapom  34361  fmlafvel  34376  fmla1  34378  gonarlem  34385  gonar  34386  goalrlem  34387  goalr  34388  satffunlem  34392  satffunlem1lem1  34393  satffunlem2lem1  34395  satffun  34400  satefvfmla1  34416  mrsubvrs  34513  mclsax  34560  3ccased  34688  dfon2lem3  34757  rdgprc  34766  cgrextend  34980  btwndiff  34999  btwnconn1lem12  35070  brsegle  35080  broutsideof2  35094  funray  35112  elicc3  35202  nn0prpwlem  35207  nn0prpw  35208  fnessref  35242  neibastop2lem  35245  filnetlem4  35266  meran1  35296  waj-ax  35299  arg-ax  35301  bj-nnclavc  35424  bj-con2com  35437  bj-axdd2  35470  bj-alrimg  35496  bj-exlimg  35500  bj-exalimi  35510  bj-cbvalimt  35516  bj-eximcom  35520  bj-ssbid1ALT  35542  bj-sb  35565  bj-snsetex  35844  bj-restpw  35973  bj-finsumval0  36166  mptsnunlem  36219  icoreclin  36238  relowlpssretop  36245  inunissunidif  36256  rdgssun  36259  finorwe  36263  domalom  36285  wl-dral1d  36400  wl-exeq  36403  wl-lem-exsb  36431  poimirlem29  36517  poimirlem32  36520  fdc  36613  seqpo  36615  incsequz  36616  isismty  36669  ismtybndlem  36674  heibor1lem  36677  ismgmOLD  36718  isexid2  36723  ghomco  36759  pridlc  36939  relcnveq3  37190  elrelscnveq3  37361  cdleme18d  39166  tendovalco  39636  cdlemn11pre  40081  dihord2pre  40096  nnadddir  41184  incssnn0  41449  fphpd  41554  jm2.19lem3  41730  setindtr  41763  islssfg2  41813  mpaaeu  41892  ordnexbtwnsuc  42017  oaabsb  42044  succlg  42078  oacl2g  42080  omabs2  42082  omcl2  42083  omcl3g  42084  pr2cv  42299  refimssco  42358  iunrelexpmin1  42459  iunrelexpmin2  42463  trclimalb2  42477  clsk1indlem3  42794  tfindsd  42964  mnurndlem1  43040  nzss  43076  sb5ALT  43286  truniALT  43302  ee223  43395  3orbi123VD  43611  sbc3orgVD  43612  exbirVD  43614  exbiriVD  43615  sbcim2gVD  43636  trsbcVD  43638  truniALTVD  43639  onfrALTlem3VD  43648  onfrALTlem2VD  43650  csbrngVD  43657  19.41rgVD  43663  ax6e2eqVD  43668  ax6e2ndeqVD  43670  2uasbanhVD  43672  sb5ALTVD  43674  vk15.4jVD  43675  infxrunb3rnmpt  44138  stoweidlem26  44742  et-equeucl  45588  hirstL-ax3  45602  rexsb  45807  rexrsb  45808  euoreqb  45817  2reu8i  45821  afvres  45880  tz6.12-afv  45881  afvco2  45884  afv2orxorb  45936  afv2res  45947  tz6.12-afv2  45948  tz6.12i-afv2  45951  dfatcolem  45963  zm1nn  46010  fzoopth  46035  2ffzoeq  46036  smonoord  46039  iccpartiltu  46090  iccpartlt  46092  iccpartltu  46093  iccpartgtl  46094  iccpartgt  46095  iccpartleu  46096  iccpartgel  46097  icceuelpart  46104  iccpartnel  46106  lswn0  46112  ichnreuop  46140  ichreuopeq  46141  prsprel  46155  sprsymrelfvlem  46158  sprsymrelf1lem  46159  sprsymrelfolem2  46161  prproropf1olem4  46174  paireqne  46179  prprelb  46184  reupr  46190  goldbachth  46215  odz2prm2pw  46231  fmtno4prmfac  46240  fmtno4prmfac193  46241  prmdvdsfmtnof1lem2  46253  2pwp1prmfmtno  46258  lighneallem2  46274  lighneallem4b  46277  lighneallem4  46278  requad2  46291  odd2prm2  46386  mogoldbblem  46388  gbepos  46426  gbowgt5  46430  gbowge7  46431  stgoldbwt  46444  sbgoldbwt  46445  sbgoldbst  46446  sbgoldbaltlem1  46447  sbgoldbalt  46449  sbgoldbo  46455  nnsum3primesle9  46462  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  bgoldbtbndlem1  46473  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  bgoldbtbnd  46477  isomuspgrlem1  46495  upgrwlkupwlk  46518  uspgrsprf1  46525  mgmhmlin  46556  issubmgm2  46560  lmod0rng  46642  rngqiprngimfo  46786  lidldomn1  46823  rnghmsscmap  46872  rnghmsubcsetclem2  46874  rngcinv  46879  rngccatidALTV  46887  rngcinvALTV  46891  funcrngcsetc  46896  funcrngcsetcALT  46897  rhmsscmap  46918  rhmsubcsetclem2  46920  rhmsubcrngclem2  46926  ringcbasbas  46932  funcringcsetc  46933  funcringcsetcALTV2lem9  46942  ringccatidALTV  46950  ringcbasbasALTV  46956  rhmsubclem4  46987  rhmsubcALTVlem4  47005  ztprmneprm  47023  pgrpgt2nabl  47042  lmodvsmdi  47058  ply1mulgsumlem2  47068  lincsumcl  47112  ellcoellss  47116  linindslinci  47129  islinindfis  47130  lincext3  47137  lindslinindimp2lem4  47142  lindslinindsimp2lem5  47143  lindslinindsimp2  47144  lindsrng01  47149  ldepspr  47154  lincresunit3lem1  47160  elfzolborelfzop1  47200  dignn0ldlem  47288  nn0sumshdiglem1  47307  1arymaptf1  47328  2arymaptf1  47339  rrx2xpref1o  47404  rrx2plord2  47408  rrx2plordisom  47409  line2ylem  47437  line2xlem  47439  line2y  47441  itschlc0xyqsol1  47452  inlinecirc02plem  47472  fullthinc  47666  tfis2d  47725  onsetrec  47753