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  365  impcom  406  impd  409  expcom  412  expdcom  413  simplbi2com  501  imdistanri  568  syldbl2  839  jaod  857  orel1  886  pm2.62  897  pm2.75  931  pm2.64  939  ccased  1036  dedlem0b  1042  3impd  1345  3expd  1350  mp3an1i  1450  minimp  1615  meredith  1635  19.35  1872  speimfw  1959  equtrr  2017  equeucl  2019  sbiedw  2304  cbv1v  2326  exsb  2349  cbv1  2395  ax12b  2417  axc11n  2419  dvelimdf  2442  equvel  2449  dfsb1  2474  sbied  2496  dfmoeu  2524  mo3  2552  mo4  2554  2mo  2636  2eu6  2645  exists2  2650  pm2.61dne  3017  rexlimdv  3142  r19.21v  3169  r19.12  3301  r19.12OLD  3302  2gencl  3505  3gencl  3506  vtocl2ga  3557  vtocl2gaf  3558  vtocl3gaf  3560  vtocl3ga  3562  vtocl4ga  3566  rspccv  3603  ceqex  3635  mob  3709  euind  3716  reuind  3745  2reu1  3887  sseq2  4003  nelss  4042  rexdifi  4142  reupick2  4320  rspn0OLD  4353  disjeq0  4457  uneqdifeq  4494  sspw  4615  ssprsseq  4830  preq12b  4853  prnebg  4858  prel12g  4866  3elpr2eq  4908  iinss2  5061  trintss  5285  dtruALT2  5370  reusv2lem1  5398  alxfr  5407  ralxfrALT  5415  exexneq  5436  dtruOLD  5443  copsexgw  5492  copsexg  5493  snopeqop  5508  propeqop  5509  opthhausdorff  5519  opthhausdorff0  5520  poclOLD  5598  pofun  5608  solin  5615  frss  5645  2optocl  5773  3optocl  5774  ssrel  5784  ssrelOLD  5785  ssrel2  5787  ssrelrel  5798  relop  5853  dfres3  5990  asymref2  6124  xpidtr  6129  trin2  6130  poltletr  6139  xp11  6181  relcnvtrg  6272  reuop  6299  tz7.7  6397  ordtr2  6415  suc11  6478  iotavalOLD  6523  funmoOLD  6570  fundif  6603  fss  6739  f0dom0  6781  fv3  6914  tz6.12i  6924  mpteqb  7023  fveqdmss  7087  eldmrexrnb  7101  funopsn  7157  funsndifnop  7160  tpres  7213  funfvima  7242  fvclss  7251  f1veqaeq  7267  isoselem  7348  oprabv  7480  ovg  7586  elovmpt3rab1  7681  sorpsscmpl  7740  iunpw  7774  trom  7880  limom  7887  peano5  7900  peano5OLD  7901  focdmex  7960  funelss  8052  funeldmdif  8053  bropopvvv  8095  bropfvvvvlem  8096  f1o2ndf1  8127  poxp  8133  soxp  8134  poxp2  8148  frxp2  8149  frxp3  8156  suppimacnv  8179  ressuppss  8188  ressuppssdif  8190  tposfn2  8254  wfr3g  8328  onnseq  8365  smoel  8381  smogt  8388  smoiso2  8390  tfr3  8420  tz7.48-2  8463  tz7.48-3  8465  tz7.49  8466  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  iiner  8808  2ecoptocl  8827  3ecoptocl  8828  undifixp  8953  xpdom2  9092  xpf1o  9164  infensuc  9180  findcard2  9189  php  9235  phpOLD  9247  onomeneqOLD  9254  isinf  9285  isinfOLD  9286  findcard2OLD  9309  unblem2  9321  infssuni  9369  finsschain  9385  fsuppunfi  9413  fsuppunbi  9414  marypha1  9459  hartogs  9569  card2on  9579  card2inf  9580  xpwdomg  9610  elirrv  9621  en3lp  9639  preleqg  9640  inf3lem1  9653  inf3lem2  9654  inf3lem3  9655  inf3lem5  9657  noinfep  9685  ttrclss  9745  ttrclselem2  9751  trcl  9753  tcel  9770  frr3g  9781  rankonidlem  9853  scottex  9910  djuunxp  9946  eldju2ndl  9949  updjud  9959  dif1card  10035  fodomnum  10082  cardaleph  10114  kmlem9  10183  kmlem13  10187  cflim2  10288  cfsmolem  10295  infpssrlem3  10330  isfin7-2  10421  fin1a2lem6  10430  fin1a2lem12  10436  domtriomlem  10467  axdc3lem4  10478  axdc4lem  10480  zorn2lem3  10523  zorn2lem4  10524  zorn2lem5  10525  zorn2lem7  10527  zornn0g  10530  axdclem2  10545  ondomon  10588  alephval2  10597  cfpwsdom  10609  wuncval2  10772  grupr  10822  gruiun  10824  ingru  10840  grothomex  10854  indpi  10932  nqereu  10954  prlem934  11058  reclem2pr  11073  mulgt0sr  11130  supsrlem  11136  dedekind  11409  lemul1a  12101  squeeze0  12150  peano5nni  12248  nnunb  12501  nn0lt2  12658  nn0le2is012  12659  fzind  12693  nn0ind-raph  12695  zindd  12696  eluzaddOLD  12890  uzin  12895  nn01to3  12958  xnn0xadd0  13261  xmulasslem  13299  icoshft  13485  fzen  13553  uzsubsubfz  13558  elfz0ubfz0  13640  elfz0fzfz0  13641  fz0fzelfz0  13642  elfzmlbp  13647  elfzodifsumelfzo  13733  ssfzo12bi  13762  fzoopth  13763  elfzonelfzo  13770  elfznelfzo  13773  injresinjlem  13788  injresinj  13789  modfzo0difsn  13944  modsumfzodifsn  13945  addmodlteq  13947  ssnn0fi  13986  fsuppmapnn0fiub0  13994  expcllem  14073  expeq0  14093  mulexp  14102  leexp2r  14174  bernneq  14227  facdiv  14282  hasheqf1oi  14346  hashnn0n0nn  14386  hashss  14404  hashgt12el  14417  hashgt12el2  14418  hashimarni  14436  hashle2pr  14474  pr2pwpr  14476  hashge2el2dif  14477  hashge2el2difr  14478  hashtpg  14482  hashge3el3dif  14483  exprelprel  14486  hash1to3  14488  fundmge2nop0  14489  fi1uzind  14494  ccatsymb  14568  swrdnd  14640  swrdnd2  14641  swrdnnn0nd  14642  swrdnd0  14643  pfxnd0  14674  swrdswrdlem  14690  swrdswrd  14691  pfxccatin12lem2a  14713  pfxccatin12lem1  14714  swrdccatin2  14715  pfxccatin12lem2  14717  pfxccatin12lem3  14718  pfxccat3  14720  swrdccat  14721  swrdccat3blem  14725  repsdf2  14764  repswswrd  14770  cshwidxmod  14789  cshwidx0  14792  cshf1  14796  cshweqrep  14807  cshw1  14808  cshwsexaOLD  14811  2cshwcshw  14812  scshwfzeqfzo  14813  cshwcsh2id  14815  wwlktovfo  14945  relexpaddg  15036  iseraltlem2  15665  modfsummods  15775  clim2prod  15870  prodfn0  15876  prodfrec  15877  prodmo  15916  fprodabs  15954  binomfallfac  16021  fprodefsum  16075  dvdsaddre2b  16287  addmodlteqALT  16305  oddge22np1  16329  nn0enne  16357  nn0o1gt2  16361  sumeven  16367  sumodd  16368  dvdslegcd  16482  gcdneg  16500  dfgcd2  16525  rplpwr  16536  lcmf  16607  lcmftp  16610  lcmfunsnlem2lem1  16612  lcmfunsnlem2  16614  lcmfdvdsb  16617  coprmdvds1  16626  qredeq  16631  coprmprod  16635  coprmproddvdslem  16636  cncongr1  16641  cncongr2  16642  prm2orodd  16665  2mulprm  16667  nnnn0modprm0  16778  prm23lt5  16786  prm23ge5  16787  dvdsprmpweqnn  16857  dvdsprmpweqle  16858  oddprmdvds  16875  prmpwdvds  16876  prmreclem4  16891  ramcl  17001  prmgaplem6  17028  prmgaplem7  17029  prmgaplem8  17030  cshwshashlem1  17068  cshwshashlem2  17069  cshwshashlem3  17070  cshwrepswhash1  17075  setsn0fun  17145  setsstruct2  17146  imasleval  17526  mreiincl  17579  mreexexd  17631  inveq  17760  cicsym  17790  cictr  17791  initoid  17993  termoid  17994  initoeu2lem0  18005  initoeu2lem1  18006  initoeu2lem2  18007  initoeu2  18008  fthestrcsetc  18144  fthsetcestrc  18159  drsdirfi  18300  isnmgm  18607  mgmhmlin  18662  issubmgm2  18666  sgrpass  18688  insubm  18778  mgm2nsgrplem3  18880  dfgrp3lem  19002  cyccom  19166  symg2bas  19359  symgfix2  19383  symgextf1  19388  gsmsymgrfix  19395  pmtrprfv3  19421  psgnunilem4  19464  efgi2  19692  0ringnnzr  20474  rnghmsscmap  20575  rnghmsubcsetclem2  20577  rngcinv  20582  funcrngcsetc  20585  funcrngcsetcALT  20586  rhmsscmap  20604  rhmsubcsetclem2  20606  rhmsubcrngclem2  20612  ringcbasbas  20618  funcringcsetc  20619  rhmsubclem4  20633  rngqiprngimfo  21208  psgndiflemB  21549  psgndiflemA  21550  elfrlmbasn0  21714  lmictra  21796  mpfrcl  22053  gsummoncoe1  22252  mamufacex  22340  matecl  22371  dmatelnd  22442  dmatscmcl  22449  scmateALT  22458  scmatsgrp1  22468  scmatf1  22477  mavmulsolcl  22497  cramerimplem1  22629  cramerimplem2  22630  pmatcollpw3fi1  22734  mp2pm2mplem4  22755  pm2mpfo  22760  chmaidscmat  22794  fvmptnn04ifb  22797  chfacfscmul0  22804  chfacfpmmul0  22808  cayhamlem1  22812  cayhamlem3  22833  cayleyhamilton1  22838  fiinopn  22847  tgcl  22916  distop  22942  isclo2  23036  iscldtop  23043  ssnei2  23064  opnnei  23068  pnfnei  23168  mnfnei  23169  tgcnp  23201  cnpnei  23212  1stcelcls  23409  txcnpi  23556  cnmptcom  23626  fbfinnfr  23789  isfildlem  23805  snfil  23812  fbunfip  23817  fgcl  23826  elfm2  23896  fmco  23909  fbflim2  23925  cnpflf2  23948  flimfcls  23974  tmdgsum  24043  neibl  24454  tngngpim  24620  fgcfil  25243  caubl  25280  volsuplem  25528  ellimc3  25852  dvnadd  25903  dvnres  25905  cpnord  25909  dvnfre  25928  ply1divex  26117  cxpmul2  26668  fsumdvdsmul  27172  zabsle1  27274  gausslemma2dlem1a  27343  gausslemma2dlem3  27346  lgsquad2lem2  27363  2lgs  27385  2sq2  27411  2sqnn0  27416  2sqnn  27417  2sqreultlem  27425  2sqreunnltlem  27428  qabvexp  27604  sltval2  27635  nolt02o  27674  ssltun1  27787  scutun12  27789  madebday  27872  mulsprop  28080  precsexlem8  28162  precsexlem9  28163  noseqind  28215  om2noseqrdg  28227  axcontlem4  28850  umgredgprv  28992  umgrnloop  28993  upgrpredgv  29024  upgredgpr  29027  edglnl  29028  usgredgprvALT  29080  usgrnloopALT  29088  usgredg2v  29112  fusgrfis  29215  nbuhgr2vtx1edgblem  29236  nb3grprlem1  29265  cusgrsize2inds  29339  cusgrfi  29344  fusgrn0degnn0  29385  uspgrloopvtxel  29402  vtxdginducedm1lem4  29428  uhgr0edg0rgrb  29460  wlkl1loop  29524  wlk1walk  29525  upgriswlk  29527  upgrwlkvtxedg  29531  uspgr2wlkeq  29532  wlkv0  29537  wlksoneq1eq2  29550  wlkon2n0  29552  wlkreslem  29555  wlkres  29556  lfgrwlkprop  29573  pthdivtx  29615  2pthnloop  29617  spthonepeq  29638  uhgrwkspthlem2  29640  uhgrwkspth  29641  usgr2wlkneq  29642  usgr2trlncl  29646  usgr2pthlem  29649  usgr2pth  29650  cyclnspth  29686  lfgrn1cycl  29688  usgr2trlncrct  29689  uspgrn2crct  29691  crctcshwlkn0lem3  29695  crctcshwlkn0lem5  29697  wwlknp  29726  wspthneq1eq2  29743  0enwwlksnge1  29747  wlklnwwlkln1  29751  wlkiswwlks2  29758  wlkiswwlksupgr2  29760  wlklnwwlkln2lem  29765  wwlksnred  29775  wwlksnextbi  29777  wwlksnredwwlkn0  29779  wwlksnextwrd  29780  wwlksnextinj  29782  wwlksnextproplem3  29794  wwlksnextprop  29795  wspthsnwspthsnon  29799  wspthsnonn0vne  29800  2pthon3v  29826  umgr2adedgwlkonALT  29830  umgr2wlk  29832  umgr2wlkon  29833  umgrwwlks2on  29840  elwspths2on  29843  usgr2wspthons3  29847  elwwlks2  29849  rusgrnumwwlk  29858  clwwlkccatlem  29871  clwlkclwwlklem2a4  29879  clwlkclwwlklem2a  29880  clwlkclwwlklem2  29882  clwlkclwwlkf1lem3  29888  erclwwlkeqlen  29901  clwwlknwwlksn  29920  loopclwwlkn1b  29924  clwwlkf1  29931  wwlksext2clwwlk  29939  eleclclwwlknlem2  29943  umgr2cwwk2dif  29946  eleclclwwlkn  29958  hashecclwwlkn1  29959  umgrhashecclwwlk  29960  clwwlknonwwlknonb  29988  clwwlknonex2lem2  29990  clwwlknonex2  29991  1pthon2v  30035  upgr3v3e3cycl  30062  uhgr3cyclexlem  30063  uhgr3cyclex  30064  eupth2lem3lem4  30113  frgr3vlem1  30155  frgr3vlem2  30156  3vfriswmgrlem  30159  3vfriswmgr  30160  3cyclfrgrrn1  30167  n4cyclfrgr  30173  frgrncvvdeqlem3  30183  frgrncvvdeqlem6  30186  frgrncvvdeqlem7  30187  frgrncvvdeqlem8  30188  frgrwopreglem4a  30192  frgrwopreglem3  30196  frgrwopreg1  30200  frgrwopreg2  30201  frgrwopreglem5lem  30202  frgrwopreglem5ALT  30204  frgrwopreg  30205  fusgr2wsp2nb  30216  2wspmdisj  30219  numclwwlk1lem2foa  30236  numclwwlk1lem2f1  30239  numclwwlk1lem2fo  30240  numclwwlk1  30243  wlkl0  30249  numclwwlk2lem1  30258  numclwlk2lem2f  30259  numclwlk2lem2f1o  30261  frgrreg  30276  frgrregord013  30277  frgrregord13  30278  friendshipgt3  30280  friendship  30281  eulplig  30367  ipassi  30723  ubthlem2  30753  isch3  31123  shintcli  31211  shmodsi  31271  spansncvi  31534  hoaddsub  31698  eigorthi  31719  pjss2coi  32046  pjnormssi  32050  pj3cor1i  32091  strb  32140  dmdmd  32182  mdsl0  32192  csmdsymi  32216  chrelat2i  32247  mdsymlem3  32287  mdsymlem6  32290  sumdmdlem2  32301  opreu2reuALT  32353  ssrelf  32484  spthcycl  34870  loop1cycl  34878  cvmlift2lem1  35043  satfrel  35108  satfrnmapom  35111  fmlafvel  35126  fmla1  35128  gonarlem  35135  gonar  35136  goalrlem  35137  goalr  35138  satffunlem  35142  satffunlem1lem1  35143  satffunlem2lem1  35145  satffun  35150  satefvfmla1  35166  mrsubvrs  35263  mclsax  35310  3ccased  35444  dfon2lem3  35512  rdgprc  35521  cgrextend  35735  btwndiff  35754  btwnconn1lem12  35825  brsegle  35835  broutsideof2  35849  funray  35867  elicc3  35932  nn0prpwlem  35937  nn0prpw  35938  fnessref  35972  neibastop2lem  35975  filnetlem4  35996  meran1  36026  waj-ax  36029  arg-ax  36031  bj-nnclavc  36154  bj-con2com  36167  bj-axdd2  36200  bj-alrimg  36226  bj-exlimg  36230  bj-exalimi  36240  bj-cbvalimt  36246  bj-eximcom  36250  bj-ssbid1ALT  36272  bj-sb  36295  bj-snsetex  36573  bj-restpw  36702  bj-finsumval0  36895  mptsnunlem  36948  icoreclin  36967  relowlpssretop  36974  inunissunidif  36985  rdgssun  36988  finorwe  36992  domalom  37014  wl-dral1d  37129  wl-exeq  37132  wl-lem-exsb  37164  poimirlem29  37253  poimirlem32  37256  fdc  37349  seqpo  37351  incsequz  37352  isismty  37405  ismtybndlem  37410  heibor1lem  37413  ismgmOLD  37454  isexid2  37459  ghomco  37495  pridlc  37675  relcnveq3  37923  elrelscnveq3  38093  cdleme18d  39898  tendovalco  40368  cdlemn11pre  40813  dihord2pre  40828  nnadddir  41980  eu6w  42236  incssnn0  42273  fphpd  42378  jm2.19lem3  42554  setindtr  42587  islssfg2  42637  mpaaeu  42716  ordnexbtwnsuc  42838  oaabsb  42865  succlg  42899  oacl2g  42901  omabs2  42903  omcl2  42904  omcl3g  42905  pr2cv  43120  refimssco  43179  iunrelexpmin1  43280  iunrelexpmin2  43284  trclimalb2  43298  clsk1indlem3  43615  tfindsd  43784  mnurndlem1  43860  nzss  43896  sb5ALT  44106  truniALT  44122  ee223  44215  3orbi123VD  44431  sbc3orgVD  44432  exbirVD  44434  exbiriVD  44435  sbcim2gVD  44456  trsbcVD  44458  truniALTVD  44459  onfrALTlem3VD  44468  onfrALTlem2VD  44470  csbrngVD  44477  19.41rgVD  44483  ax6e2eqVD  44488  ax6e2ndeqVD  44490  2uasbanhVD  44492  sb5ALTVD  44494  vk15.4jVD  44495  infxrunb3rnmpt  44948  stoweidlem26  45552  et-equeucl  46398  hirstL-ax3  46412  rexsb  46617  rexrsb  46618  euoreqb  46627  2reu8i  46631  afvres  46690  tz6.12-afv  46691  afvco2  46694  afv2orxorb  46746  afv2res  46757  tz6.12-afv2  46758  tz6.12i-afv2  46761  dfatcolem  46773  zm1nn  46820  2ffzoeq  46845  smonoord  46848  iccpartiltu  46899  iccpartlt  46901  iccpartltu  46902  iccpartgtl  46903  iccpartgt  46904  iccpartleu  46905  iccpartgel  46906  icceuelpart  46913  iccpartnel  46915  lswn0  46921  ichnreuop  46949  ichreuopeq  46950  prsprel  46964  sprsymrelfvlem  46967  sprsymrelf1lem  46968  sprsymrelfolem2  46970  prproropf1olem4  46983  paireqne  46988  prprelb  46993  reupr  46999  goldbachth  47024  odz2prm2pw  47040  fmtno4prmfac  47049  fmtno4prmfac193  47050  prmdvdsfmtnof1lem2  47062  2pwp1prmfmtno  47067  lighneallem2  47083  lighneallem4b  47086  lighneallem4  47087  requad2  47100  odd2prm2  47195  mogoldbblem  47197  gbepos  47235  gbowgt5  47239  gbowge7  47240  stgoldbwt  47253  sbgoldbwt  47254  sbgoldbst  47255  sbgoldbaltlem1  47256  sbgoldbalt  47258  sbgoldbo  47264  nnsum3primesle9  47271  nnsum4primesodd  47273  nnsum4primesoddALTV  47274  nnsum4primeseven  47277  nnsum4primesevenALTV  47278  bgoldbtbndlem1  47282  bgoldbtbndlem2  47283  bgoldbtbndlem3  47284  bgoldbtbnd  47286  dfnbgr6  47329  isuspgrimlem  47358  upgrwlkupwlk  47388  uspgrsprf1  47395  lmod0rng  47477  lidldomn1  47479  rngccatidALTV  47520  rngcinvALTV  47524  rhmsubcALTVlem4  47532  funcringcsetcALTV2lem9  47546  ringccatidALTV  47554  ringcbasbasALTV  47560  ztprmneprm  47597  pgrpgt2nabl  47616  lmodvsmdi  47632  ply1mulgsumlem2  47641  lincsumcl  47685  ellcoellss  47689  linindslinci  47702  islinindfis  47703  lincext3  47710  lindslinindimp2lem4  47715  lindslinindsimp2lem5  47716  lindslinindsimp2  47717  lindsrng01  47722  ldepspr  47727  lincresunit3lem1  47733  elfzolborelfzop1  47773  dignn0ldlem  47861  nn0sumshdiglem1  47880  1arymaptf1  47901  2arymaptf1  47912  rrx2xpref1o  47977  rrx2plord2  47981  rrx2plordisom  47982  line2ylem  48010  line2xlem  48012  line2y  48014  itschlc0xyqsol1  48025  inlinecirc02plem  48045  fullthinc  48238  tfis2d  48297  onsetrec  48325