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  366  impcom  407  impd  410  expcom  413  expdcom  414  simplbi2com  502  imdistanri  569  syldbl2  837  jaod  855  orel1  885  pm2.62  896  pm2.75  930  pm2.64  938  ccased  1035  dedlem0b  1041  3impd  1346  3expd  1351  mp3an1i  1452  norassOLD  1536  minimp  1625  meredith  1645  19.35  1881  speimfw  1968  equtrr  2026  equeucl  2028  sbiedw  2313  sbiedwOLD  2314  cbv1v  2335  exsb  2357  cbv1  2402  ax12b  2424  axc11n  2426  dvelimdf  2449  equvel  2456  dfsb1  2485  sbied  2507  dfmoeu  2536  mo3  2564  mo4  2566  2mo  2650  2eu6  2658  exists2  2663  pm2.61dne  3030  rexlimdv  3211  r19.12  3252  r19.12OLD  3253  2gencl  3462  3gencl  3463  vtocl2ga  3504  rspccv  3549  ceqex  3574  mob  3647  euind  3654  reuind  3683  2reu1  3826  sseq2  3943  nelss  3980  rexdifi  4076  reupick2  4251  rspn0OLD  4284  disjeq0  4386  uneqdifeq  4420  sspw  4543  ssprsseq  4755  preq12b  4778  prnebg  4783  prel12g  4791  3elpr2eq  4835  iinss2  4983  trintss  5204  dtru  5288  reusv2lem1  5316  alxfr  5325  ralxfrALT  5333  copsexgw  5398  copsexg  5399  snopeqop  5414  propeqop  5415  opthhausdorff  5425  opthhausdorff0  5426  poclOLD  5502  pofun  5512  solin  5519  frss  5547  2optocl  5672  3optocl  5673  ssrel  5683  ssrel2  5685  ssrelrel  5695  relop  5748  dfres3  5885  asymref2  6011  xpidtr  6016  trin2  6017  poltletr  6026  xp11  6067  relcnvtrg  6159  reuop  6185  tz7.7  6277  ordtr2  6295  suc11  6354  iotaval  6392  funmo  6434  fundif  6467  fss  6601  f0dom0  6642  fv3  6774  tz6.12i  6782  mpteqb  6876  fveqdmss  6938  eldmrexrnb  6950  funopsn  7002  funsndifnop  7005  tpres  7058  funfvima  7088  fvclss  7097  f1veqaeq  7111  isoselem  7192  oprabv  7313  ovg  7415  elovmpt3rab1  7507  sorpsscmpl  7565  iunpw  7599  trom  7696  limom  7703  peano5  7714  peano5OLD  7715  fornex  7772  funelss  7861  funeldmdif  7862  bropopvvv  7901  bropfvvvvlem  7902  f1o2ndf1  7934  poxp  7940  soxp  7941  suppimacnv  7961  ressuppss  7970  ressuppssdif  7972  tposfn2  8035  wfr3g  8109  onnseq  8146  smoel  8162  smogt  8169  smoiso2  8171  tfr3  8201  tz7.48-2  8243  tz7.48-3  8245  tz7.49  8246  oecl  8329  oaordex  8351  oalimcl  8353  oaass  8354  omordi  8359  omlimcl  8371  odi  8372  omeulem1  8375  oen0  8379  nnawordi  8414  nnaass  8415  nnmordi  8424  omabs  8441  omsmolem  8447  iiner  8536  2ecoptocl  8555  3ecoptocl  8556  undifixp  8680  xpdom2  8807  xpf1o  8875  infensuc  8891  php  8897  findcard2  8909  onomeneq  8943  isinf  8965  findcard2OLD  8986  unblem2  8997  infssuni  9040  finsschain  9056  fsuppunfi  9078  fsuppunbi  9079  marypha1  9123  hartogs  9233  card2on  9243  card2inf  9244  xpwdomg  9274  elirrv  9285  en3lp  9302  preleqg  9303  inf3lem1  9316  inf3lem2  9317  inf3lem3  9318  inf3lem5  9320  noinfep  9348  trpredmintr  9409  trpredrec  9415  trcl  9417  tcel  9434  frr3g  9445  rankonidlem  9517  scottex  9574  djuunxp  9610  eldju2ndl  9613  updjud  9623  dif1card  9697  fodomnum  9744  cardaleph  9776  kmlem9  9845  kmlem13  9849  cflim2  9950  cfsmolem  9957  infpssrlem3  9992  isfin7-2  10083  fin1a2lem6  10092  fin1a2lem12  10098  domtriomlem  10129  axdc3lem4  10140  axdc4lem  10142  zorn2lem3  10185  zorn2lem4  10186  zorn2lem5  10187  zorn2lem7  10189  zornn0g  10192  axdclem2  10207  ondomon  10250  alephval2  10259  cfpwsdom  10271  wuncval2  10434  grupr  10484  gruiun  10486  ingru  10502  grothomex  10516  indpi  10594  nqereu  10616  prlem934  10720  reclem2pr  10735  mulgt0sr  10792  supsrlem  10798  dedekind  11068  lemul1a  11759  squeeze0  11808  peano5nni  11906  nnunb  12159  nn0lt2  12313  nn0le2is012  12314  fzind  12348  nn0ind-raph  12350  zindd  12351  eluzadd  12542  uzin  12547  nn01to3  12610  xnn0xadd0  12910  xmulasslem  12948  icoshft  13134  fzen  13202  uzsubsubfz  13207  elfz0ubfz0  13289  elfz0fzfz0  13290  fz0fzelfz0  13291  elfzmlbp  13296  elfzodifsumelfzo  13381  ssfzo12bi  13410  elfzonelfzo  13417  elfznelfzo  13420  injresinjlem  13435  injresinj  13436  modfzo0difsn  13591  modsumfzodifsn  13592  addmodlteq  13594  ssnn0fi  13633  fsuppmapnn0fiub0  13641  expcllem  13721  expeq0  13741  mulexp  13750  leexp2r  13820  bernneq  13872  facdiv  13929  hasheqf1oi  13994  hashnn0n0nn  14034  hashss  14052  hashgt12el  14065  hashgt12el2  14066  hashimarni  14084  hashle2pr  14119  pr2pwpr  14121  hashge2el2dif  14122  hashge2el2difr  14123  hashtpg  14127  hashge3el3dif  14128  exprelprel  14131  hash1to3  14133  fundmge2nop0  14134  fi1uzind  14139  ccatsymb  14215  swrdnd  14295  swrdnd2  14296  swrdnnn0nd  14297  swrdnd0  14298  pfxnd0  14329  swrdswrdlem  14345  swrdswrd  14346  pfxccatin12lem2a  14368  pfxccatin12lem1  14369  swrdccatin2  14370  pfxccatin12lem2  14372  pfxccatin12lem3  14373  pfxccat3  14375  swrdccat  14376  swrdccat3blem  14380  repsdf2  14419  repswswrd  14425  cshwidxmod  14444  cshwidx0  14447  cshf1  14451  cshweqrep  14462  cshw1  14463  cshwsexa  14465  2cshwcshw  14466  scshwfzeqfzo  14467  cshwcsh2id  14469  wwlktovfo  14601  relexpaddg  14692  iseraltlem2  15322  modfsummods  15433  clim2prod  15528  prodfn0  15534  prodfrec  15535  prodmo  15574  fprodabs  15612  binomfallfac  15679  fprodefsum  15732  dvdsaddre2b  15944  addmodlteqALT  15962  oddge22np1  15986  nn0enne  16014  nn0o1gt2  16018  sumeven  16024  sumodd  16025  dvdslegcd  16139  gcdneg  16157  dfgcd2  16182  rplpwr  16195  lcmf  16266  lcmftp  16269  lcmfunsnlem2lem1  16271  lcmfunsnlem2  16273  lcmfdvdsb  16276  coprmdvds1  16285  qredeq  16290  coprmprod  16294  coprmproddvdslem  16295  cncongr1  16300  cncongr2  16301  prm2orodd  16324  2mulprm  16326  nnnn0modprm0  16435  prm23lt5  16443  prm23ge5  16444  dvdsprmpweqnn  16514  dvdsprmpweqle  16515  oddprmdvds  16532  prmpwdvds  16533  prmreclem4  16548  ramcl  16658  prmgaplem6  16685  prmgaplem7  16686  prmgaplem8  16687  cshwshashlem1  16725  cshwshashlem2  16726  cshwshashlem3  16727  cshwrepswhash1  16732  setsn0fun  16802  setsstruct2  16803  imasleval  17169  mreiincl  17222  mreexexd  17274  inveq  17403  cicsym  17433  cictr  17434  initoid  17632  termoid  17633  initoeu2lem0  17644  initoeu2lem1  17645  initoeu2lem2  17646  initoeu2  17647  fthestrcsetc  17783  fthsetcestrc  17798  drsdirfi  17938  isnmgm  18245  sgrpass  18296  insubm  18372  mgm2nsgrplem3  18474  dfgrp3lem  18588  cyccom  18737  symg2bas  18915  symgfix2  18939  symgextf1  18944  gsmsymgrfix  18951  pmtrprfv3  18977  psgnunilem4  19020  efgi2  19246  0ringnnzr  20453  psgndiflemB  20717  psgndiflemA  20718  elfrlmbasn0  20880  lmictra  20962  mpfrcl  21205  gsummoncoe1  21385  mamufacex  21448  matecl  21482  dmatelnd  21553  dmatscmcl  21560  scmateALT  21569  scmatsgrp1  21579  scmatf1  21588  mavmulsolcl  21608  cramerimplem1  21740  cramerimplem2  21741  pmatcollpw3fi1  21845  mp2pm2mplem4  21866  pm2mpfo  21871  chmaidscmat  21905  fvmptnn04ifb  21908  chfacfscmul0  21915  chfacfpmmul0  21919  cayhamlem1  21923  cayhamlem3  21944  cayleyhamilton1  21949  fiinopn  21958  tgcl  22027  distop  22053  isclo2  22147  iscldtop  22154  ssnei2  22175  opnnei  22179  pnfnei  22279  mnfnei  22280  tgcnp  22312  cnpnei  22323  1stcelcls  22520  txcnpi  22667  cnmptcom  22737  fbfinnfr  22900  isfildlem  22916  snfil  22923  fbunfip  22928  fgcl  22937  elfm2  23007  fmco  23020  fbflim2  23036  cnpflf2  23059  flimfcls  23085  tmdgsum  23154  neibl  23563  tngngpim  23729  fgcfil  24340  caubl  24377  volsuplem  24624  ellimc3  24948  dvnadd  24998  dvnres  25000  cpnord  25004  dvnfre  25021  ply1divex  25206  cxpmul2  25749  zabsle1  26349  gausslemma2dlem1a  26418  gausslemma2dlem3  26421  lgsquad2lem2  26438  2lgs  26460  2sq2  26486  2sqnn0  26491  2sqnn  26492  2sqreultlem  26500  2sqreunnltlem  26503  qabvexp  26679  axcontlem4  27238  umgredgprv  27380  umgrnloop  27381  upgrpredgv  27412  upgredgpr  27415  edglnl  27416  usgredgprvALT  27465  usgrnloopALT  27473  usgredg2v  27497  fusgrfis  27600  nbuhgr2vtx1edgblem  27621  nb3grprlem1  27650  cusgrsize2inds  27723  cusgrfi  27728  fusgrn0degnn0  27769  uspgrloopvtxel  27786  vtxdginducedm1lem4  27812  uhgr0edg0rgrb  27844  wlkl1loop  27907  wlk1walk  27908  upgriswlk  27910  upgrwlkvtxedg  27914  uspgr2wlkeq  27915  wlkv0  27920  wlklenvclwlkOLD  27925  wlksoneq1eq2  27934  wlkon2n0  27936  wlkreslem  27939  wlkres  27940  lfgrwlkprop  27957  pthdivtx  27998  2pthnloop  28000  spthonepeq  28021  uhgrwkspthlem2  28023  uhgrwkspth  28024  usgr2wlkneq  28025  usgr2trlncl  28029  usgr2pthlem  28032  usgr2pth  28033  cyclnspth  28069  lfgrn1cycl  28071  usgr2trlncrct  28072  uspgrn2crct  28074  crctcshwlkn0lem3  28078  crctcshwlkn0lem5  28080  wwlknp  28109  wspthneq1eq2  28126  0enwwlksnge1  28130  wlklnwwlkln1  28134  wlkiswwlks2  28141  wlkiswwlksupgr2  28143  wlklnwwlkln2lem  28148  wwlksnred  28158  wwlksnextbi  28160  wwlksnredwwlkn0  28162  wwlksnextwrd  28163  wwlksnextinj  28165  wwlksnextproplem3  28177  wwlksnextprop  28178  wspthsnwspthsnon  28182  wspthsnonn0vne  28183  2pthon3v  28209  umgr2adedgwlkonALT  28213  umgr2wlk  28215  umgr2wlkon  28216  umgrwwlks2on  28223  elwspths2on  28226  usgr2wspthons3  28230  elwwlks2  28232  rusgrnumwwlk  28241  clwwlkccatlem  28254  clwlkclwwlklem2a4  28262  clwlkclwwlklem2a  28263  clwlkclwwlklem2  28265  clwlkclwwlkf1lem3  28271  erclwwlkeqlen  28284  clwwlknwwlksn  28303  loopclwwlkn1b  28307  clwwlkf1  28314  wwlksext2clwwlk  28322  eleclclwwlknlem2  28326  umgr2cwwk2dif  28329  eleclclwwlkn  28341  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  clwwlknonwwlknonb  28371  clwwlknonex2lem2  28373  clwwlknonex2  28374  1pthon2v  28418  upgr3v3e3cycl  28445  uhgr3cyclexlem  28446  uhgr3cyclex  28447  eupth2lem3lem4  28496  frgr3vlem1  28538  frgr3vlem2  28539  3vfriswmgrlem  28542  3vfriswmgr  28543  3cyclfrgrrn1  28550  n4cyclfrgr  28556  frgrncvvdeqlem3  28566  frgrncvvdeqlem6  28569  frgrncvvdeqlem7  28570  frgrncvvdeqlem8  28571  frgrwopreglem4a  28575  frgrwopreglem3  28579  frgrwopreg1  28583  frgrwopreg2  28584  frgrwopreglem5lem  28585  frgrwopreglem5ALT  28587  frgrwopreg  28588  fusgr2wsp2nb  28599  2wspmdisj  28602  numclwwlk1lem2foa  28619  numclwwlk1lem2f1  28622  numclwwlk1lem2fo  28623  numclwwlk1  28626  wlkl0  28632  numclwwlk2lem1  28641  numclwlk2lem2f  28642  numclwlk2lem2f1o  28644  frgrreg  28659  frgrregord013  28660  frgrregord13  28661  friendshipgt3  28663  friendship  28664  eulplig  28748  ipassi  29104  ubthlem2  29134  isch3  29504  shintcli  29592  shmodsi  29652  spansncvi  29915  hoaddsub  30079  eigorthi  30100  pjss2coi  30427  pjnormssi  30431  pj3cor1i  30472  strb  30521  dmdmd  30563  mdsl0  30573  csmdsymi  30597  chrelat2i  30628  mdsymlem3  30668  mdsymlem6  30671  sumdmdlem2  30682  opreu2reuALT  30726  ssrelf  30856  spthcycl  32991  loop1cycl  32999  cvmlift2lem1  33164  satfrel  33229  satfrnmapom  33232  fmlafvel  33247  fmla1  33249  gonarlem  33256  gonar  33257  goalrlem  33258  goalr  33259  satffunlem  33263  satffunlem1lem1  33264  satffunlem2lem1  33266  satffun  33271  satefvfmla1  33287  mrsubvrs  33384  mclsax  33431  3ccased  33565  dfon2lem3  33667  rdgprc  33676  ttrclss  33706  ttrclselem2  33712  poxp2  33717  frxp2  33718  frxp3  33724  sexp3  33726  naddssim  33764  sltval2  33786  nolt02o  33825  ssltun1  33929  scutun12  33931  madebday  34007  cgrextend  34237  btwndiff  34256  btwnconn1lem12  34327  brsegle  34337  broutsideof2  34351  funray  34369  elicc3  34433  nn0prpwlem  34438  nn0prpw  34439  fnessref  34473  neibastop2lem  34476  filnetlem4  34497  meran1  34527  waj-ax  34530  arg-ax  34532  bj-nnclavc  34655  bj-con2com  34668  bj-axdd2  34701  bj-alrimg  34727  bj-exlimg  34731  bj-exalimi  34741  bj-cbvalimt  34747  bj-eximcom  34751  bj-ssbid1ALT  34773  bj-sb  34796  bj-dtru  34926  bj-snsetex  35080  bj-restpw  35190  bj-finsumval0  35383  mptsnunlem  35436  icoreclin  35455  relowlpssretop  35462  inunissunidif  35473  rdgssun  35476  finorwe  35480  domalom  35502  wl-dral1d  35617  wl-exeq  35620  wl-lem-exsb  35648  poimirlem29  35733  poimirlem32  35736  fdc  35830  seqpo  35832  incsequz  35833  isismty  35886  ismtybndlem  35891  heibor1lem  35894  ismgmOLD  35935  isexid2  35940  ghomco  35976  pridlc  36156  relcnveq3  36383  elrelscnveq3  36536  cdleme18d  38236  tendovalco  38706  cdlemn11pre  39151  dihord2pre  39166  nnadddir  40221  incssnn0  40449  fphpd  40554  jm2.19lem3  40729  setindtr  40762  islssfg2  40812  mpaaeu  40891  pr2cv  41044  refimssco  41104  iunrelexpmin1  41205  iunrelexpmin2  41209  trclimalb2  41223  clsk1indlem3  41542  tfindsd  41712  mnurndlem1  41788  nzss  41824  sb5ALT  42034  truniALT  42050  ee223  42143  3orbi123VD  42359  sbc3orgVD  42360  exbirVD  42362  exbiriVD  42363  sbcim2gVD  42384  trsbcVD  42386  truniALTVD  42387  onfrALTlem3VD  42396  onfrALTlem2VD  42398  csbrngVD  42405  19.41rgVD  42411  ax6e2eqVD  42416  ax6e2ndeqVD  42418  2uasbanhVD  42420  sb5ALTVD  42422  vk15.4jVD  42423  infxrunb3rnmpt  42858  stoweidlem26  43457  hirstL-ax3  44274  rexsb  44478  rexrsb  44479  euoreqb  44488  2reu8i  44492  afvres  44551  tz6.12-afv  44552  afvco2  44555  afv2orxorb  44607  afv2res  44618  tz6.12-afv2  44619  tz6.12i-afv2  44622  dfatcolem  44634  zm1nn  44682  fzoopth  44707  2ffzoeq  44708  smonoord  44711  iccpartiltu  44762  iccpartlt  44764  iccpartltu  44765  iccpartgtl  44766  iccpartgt  44767  iccpartleu  44768  iccpartgel  44769  icceuelpart  44776  iccpartnel  44778  lswn0  44784  ichnreuop  44812  ichreuopeq  44813  prsprel  44827  sprsymrelfvlem  44830  sprsymrelf1lem  44831  sprsymrelfolem2  44833  prproropf1olem4  44846  paireqne  44851  prprelb  44856  reupr  44862  goldbachth  44887  odz2prm2pw  44903  fmtno4prmfac  44912  fmtno4prmfac193  44913  prmdvdsfmtnof1lem2  44925  2pwp1prmfmtno  44930  lighneallem2  44946  lighneallem4b  44949  lighneallem4  44950  requad2  44963  odd2prm2  45058  mogoldbblem  45060  gbepos  45098  gbowgt5  45102  gbowge7  45103  stgoldbwt  45116  sbgoldbwt  45117  sbgoldbst  45118  sbgoldbaltlem1  45119  sbgoldbalt  45121  sbgoldbo  45127  nnsum3primesle9  45134  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  bgoldbtbndlem1  45145  bgoldbtbndlem2  45146  bgoldbtbndlem3  45147  bgoldbtbnd  45149  isomuspgrlem1  45167  upgrwlkupwlk  45190  uspgrsprf1  45197  mgmhmlin  45228  issubmgm2  45232  lmod0rng  45314  lidldomn1  45367  lidlmmgm  45371  rnghmsscmap  45420  rnghmsubcsetclem2  45422  rngcinv  45427  rngccatidALTV  45435  rngcinvALTV  45439  funcrngcsetc  45444  funcrngcsetcALT  45445  rhmsscmap  45466  rhmsubcsetclem2  45468  rhmsubcrngclem2  45474  ringcinv  45478  ringcbasbas  45480  funcringcsetc  45481  funcringcsetcALTV2lem9  45490  ringccatidALTV  45498  ringcinvALTV  45502  ringcbasbasALTV  45504  rhmsubclem4  45535  rhmsubcALTVlem4  45553  ztprmneprm  45571  pgrpgt2nabl  45590  lmodvsmdi  45606  ply1mulgsumlem2  45616  lincsumcl  45660  ellcoellss  45664  linindslinci  45677  islinindfis  45678  lincext3  45685  lindslinindimp2lem4  45690  lindslinindsimp2lem5  45691  lindslinindsimp2  45692  lindsrng01  45697  ldepspr  45702  lincresunit3lem1  45708  elfzolborelfzop1  45748  dignn0ldlem  45836  nn0sumshdiglem1  45855  1arymaptf1  45876  2arymaptf1  45887  rrx2xpref1o  45952  rrx2plord2  45956  rrx2plordisom  45957  line2ylem  45985  line2xlem  45987  line2y  45989  itschlc0xyqsol1  46000  inlinecirc02plem  46020  fullthinc  46215  tfis2d  46272  onsetrec  46299