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  842  jaod  860  orel1  889  pm2.62  900  pm2.75  934  pm2.64  944  ccased  1039  dedlem0b  1045  3impd  1350  3expd  1355  mp3an1i  1457  minimp  1623  meredith  1643  19.35  1879  speimfw  1965  equtrr  2024  equeucl  2026  ax12ev2  2188  sbiedw  2322  cbv1v  2341  exsb  2364  cbv1  2407  ax12b  2429  axc11n  2431  dvelimdf  2454  equvel  2461  dfsb1  2486  sbied  2508  dfmoeu  2536  mo3  2565  mo4  2567  2mo  2649  2eu6  2658  exists2  2663  pm2.61dne  3019  rexlimdv  3137  r19.21v  3163  r19.12  3287  2gencl  3473  3gencl  3474  vtocl2ga  3522  vtocl2gaf  3523  vtocl3gaf  3525  vtocl3ga  3527  vtocl4ga  3530  rspccv  3562  ceqex  3595  mob  3664  euind  3671  reuind  3700  2reu1  3836  sseq2  3949  nelss  3988  rexdifi  4091  reupick2  4272  disjeq0  4397  uneqdifeq  4433  sspw  4553  ssprsseq  4769  preq12b  4794  prnebg  4800  prel12g  4808  3elpr2eq  4850  iinss2  5001  trintss  5211  dtruALT2  5307  reusv2lem1  5335  alxfr  5344  ralxfrALT  5352  exexneq  5382  copsexgw  5438  copsexg  5439  snopeqop  5454  propeqop  5455  opthhausdorff  5465  opthhausdorff0  5466  pofun  5550  solin  5559  frss  5588  2optocl  5720  3optocl  5721  ssrel  5732  ssrel2  5734  ssrelrel  5745  relop  5799  dfres3  5943  asymref2  6074  xpidtr  6079  trin2  6080  poltletr  6089  imadifssran  6109  xp11  6133  relcnvtrg  6225  reuop  6251  tz7.7  6343  ordtr2  6362  suc11  6426  fundif  6541  fss  6678  f0dom0  6718  fv3  6852  tz6.12i  6860  mpteqb  6961  fveqdmss  7024  eldmrexrnb  7038  funopsn  7095  funsndifnop  7098  tpres  7149  funfvima  7178  fvclss  7189  f1veqaeq  7204  fvf1pr  7255  isoselem  7289  oprabv  7420  ovg  7525  elovmpt3rab1  7620  sorpsscmpl  7681  iunpw  7718  trom  7819  limom  7826  peano5  7837  focdmex  7902  funelss  7993  funeldmdif  7994  bropopvvv  8033  bropfvvvvlem  8034  f1o2ndf1  8065  poxp  8071  soxp  8072  poxp2  8086  frxp2  8087  frxp3  8094  suppimacnv  8117  ressuppss  8126  ressuppssdif  8128  tposfn2  8191  wfr3g  8262  onnseq  8277  smoel  8293  smogt  8300  smoiso2  8302  tfr3  8331  tz7.48-2  8374  tz7.48-3  8376  tz7.49  8377  oecl  8465  oaordex  8486  oalimcl  8488  oaass  8489  omordi  8494  omlimcl  8506  odi  8507  omeulem1  8510  oen0  8515  nnawordi  8550  nnaass  8551  nnmordi  8560  omabs  8580  omsmolem  8586  naddssim  8614  brinxper  8666  iiner  8729  2ecoptocl  8748  3ecoptocl  8749  undifixp  8875  xpdom2  9003  xpf1o  9070  infensuc  9086  findcard2  9092  php  9134  isinf  9168  unblem2  9196  fodomfir  9231  infssuni  9249  finsschain  9262  fsuppunfi  9294  fsuppunbi  9295  marypha1  9340  hartogs  9452  card2on  9462  card2inf  9463  xpwdomg  9493  elirrv  9505  elirrvOLD  9506  en3lp  9526  preleqg  9527  inf3lem1  9540  inf3lem2  9541  inf3lem3  9542  inf3lem5  9544  noinfep  9572  ttrclss  9632  ttrclselem2  9638  trcl  9640  tcel  9655  frr3g  9671  rankonidlem  9743  scottex  9800  djuunxp  9836  eldju2ndl  9839  updjud  9849  dif1card  9923  fodomnum  9970  cardaleph  10002  kmlem9  10072  kmlem13  10076  cflim2  10176  cfsmolem  10183  infpssrlem3  10218  isfin7-2  10309  fin1a2lem6  10318  fin1a2lem12  10324  domtriomlem  10355  axdc3lem4  10366  axdc4lem  10368  zorn2lem3  10411  zorn2lem4  10412  zorn2lem5  10413  zorn2lem7  10415  zornn0g  10418  axdclem2  10433  ondomon  10476  alephval2  10486  cfpwsdom  10498  wuncval2  10661  grupr  10711  gruiun  10713  ingru  10729  grothomex  10743  indpi  10821  nqereu  10843  prlem934  10947  reclem2pr  10962  mulgt0sr  11019  supsrlem  11025  1re  11135  dedekind  11300  lemul1a  12000  squeeze0  12050  peano5nni  12168  nnadddir  12224  nnunb  12424  nn0lt2  12583  nn0le2is012  12584  fzind  12618  nn0ind-raph  12620  zindd  12621  uzin  12815  nn01to3  12882  xnn0xadd0  13190  xmulasslem  13228  icoshft  13417  fzen  13486  uzsubsubfz  13491  elfz0ubfz0  13577  elfz0fzfz0  13578  fz0fzelfz0  13579  elfzmlbp  13584  elfzodifsumelfzo  13677  ssfzo12bi  13707  fzoopth  13708  elfzonelfzo  13715  elfznelfzo  13719  injresinjlem  13736  injresinj  13737  modfzo0difsn  13896  modsumfzodifsn  13897  addmodlteq  13899  ssnn0fi  13938  fsuppmapnn0fiub0  13946  expcllem  14025  expeq0  14045  mulexp  14054  leexp2r  14127  bernneq  14182  facdiv  14240  hasheqf1oi  14304  hashnn0n0nn  14344  hashss  14362  hashgt12el  14375  hashgt12el2  14376  hashimarni  14394  hashle2pr  14430  pr2pwpr  14432  hashge2el2dif  14433  hashge2el2difr  14434  hashtpg  14438  hashge3el3dif  14440  exprelprel  14443  hash1to3  14445  hash3tpde  14446  tpfo  14453  fundmge2nop0  14455  fi1uzind  14460  ccatsymb  14536  swrdnd  14608  swrdnd2  14609  swrdnnn0nd  14610  swrdnd0  14611  pfxnd0  14642  swrdswrdlem  14657  swrdswrd  14658  pfxccatin12lem2a  14680  pfxccatin12lem1  14681  swrdccatin2  14682  pfxccatin12lem2  14684  pfxccatin12lem3  14685  pfxccat3  14687  swrdccat  14688  swrdccat3blem  14692  repsdf2  14731  repswswrd  14737  cshwidxmod  14756  cshwidx0  14759  cshf1  14763  cshweqrep  14774  cshw1  14775  2cshwcshw  14778  scshwfzeqfzo  14779  cshwcsh2id  14781  wwlktovfo  14911  relexpaddg  15006  iseraltlem2  15636  modfsummods  15747  clim2prod  15844  prodfn0  15850  prodfrec  15851  prodmo  15892  fprodabs  15930  binomfallfac  15997  fprodefsum  16051  dvdsaddre2b  16267  addmodlteqALT  16285  oddge22np1  16309  nn0enne  16337  nn0o1gt2  16341  sumeven  16347  sumodd  16348  dvdslegcd  16464  gcdneg  16482  dfgcd2  16506  rplpwr  16518  lcmf  16593  lcmftp  16596  lcmfunsnlem2lem1  16598  lcmfunsnlem2  16600  lcmfdvdsb  16603  coprmdvds1  16612  qredeq  16617  coprmprod  16621  coprmproddvdslem  16622  cncongr1  16627  cncongr2  16628  prm2orodd  16651  2mulprm  16653  nnnn0modprm0  16768  prm23lt5  16776  prm23ge5  16777  dvdsprmpweqnn  16847  dvdsprmpweqle  16848  oddprmdvds  16865  prmpwdvds  16866  prmreclem4  16881  ramcl  16991  prmgaplem6  17018  prmgaplem7  17019  prmgaplem8  17020  cshwshashlem1  17057  cshwshashlem2  17058  cshwshashlem3  17059  cshwrepswhash1  17064  setsn0fun  17134  setsstruct2  17135  imasleval  17496  mreiincl  17549  mreexexd  17605  inveq  17732  cicsym  17762  cictr  17763  initoid  17959  termoid  17960  initoeu2lem0  17971  initoeu2lem1  17972  initoeu2lem2  17973  initoeu2  17974  fthestrcsetc  18107  fthsetcestrc  18122  drsdirfi  18262  isnmgm  18603  mgmhmlin  18658  issubmgm2  18662  sgrpass  18684  insubm  18777  mgm2nsgrplem3  18882  dfgrp3lem  19005  cyccom  19169  symg2bas  19359  symgfix2  19382  symgextf1  19387  gsmsymgrfix  19394  pmtrprfv3  19420  psgnunilem4  19463  efgi2  19691  0ringnnzr  20493  rnghmsscmap  20598  rnghmsubcsetclem2  20600  rngcinv  20605  funcrngcsetc  20608  funcrngcsetcALT  20609  rhmsscmap  20627  rhmsubcsetclem2  20629  rhmsubcrngclem2  20635  ringcbasbas  20641  funcringcsetc  20642  rhmsubclem4  20656  rngqiprngimfo  21291  psgndiflemB  21590  psgndiflemA  21591  elfrlmbasn0  21753  lmictra  21835  mpfrcl  22073  gsummoncoe1  22283  mamufacex  22371  matecl  22400  dmatelnd  22471  dmatscmcl  22478  scmateALT  22487  scmatsgrp1  22497  scmatf1  22506  mavmulsolcl  22526  cramerimplem1  22658  cramerimplem2  22659  pmatcollpw3fi1  22763  mp2pm2mplem4  22784  pm2mpfo  22789  chmaidscmat  22823  fvmptnn04ifb  22826  chfacfscmul0  22833  chfacfpmmul0  22837  cayhamlem1  22841  cayhamlem3  22862  cayleyhamilton1  22867  fiinopn  22876  tgcl  22944  distop  22970  isclo2  23063  iscldtop  23070  ssnei2  23091  opnnei  23095  pnfnei  23195  mnfnei  23196  tgcnp  23228  cnpnei  23239  1stcelcls  23436  txcnpi  23583  cnmptcom  23653  fbfinnfr  23816  isfildlem  23832  snfil  23839  fbunfip  23844  fgcl  23853  elfm2  23923  fmco  23936  fbflim2  23952  cnpflf2  23975  flimfcls  24001  tmdgsum  24070  neibl  24476  tngngpim  24634  fgcfil  25248  caubl  25285  volsuplem  25532  ellimc3  25856  dvnadd  25906  dvnres  25908  cpnord  25912  dvnfre  25929  ply1divex  26112  cxpmul2  26666  fsumdvdsmul  27172  zabsle1  27273  gausslemma2dlem1a  27342  gausslemma2dlem3  27345  lgsquad2lem2  27362  2lgs  27384  2sq2  27410  2sqnn0  27415  2sqnn  27416  2sqreultlem  27424  2sqreunnltlem  27427  qabvexp  27603  ltsval2  27634  nolt02o  27673  sltsun1  27794  cutsun12  27796  madebday  27906  mulsprop  28136  precsexlem8  28220  precsexlem9  28221  noseqind  28298  om2noseqrdg  28310  n0cutlt  28365  peano5uzs  28410  expadds  28441  bdaypw2n0bndlem  28469  bdaypw2n0bnd  28470  axcontlem4  29050  umgredgprv  29190  umgrnloop  29191  upgrpredgv  29222  upgredgpr  29225  edglnl  29226  usgredgprvALT  29278  usgrnloopALT  29286  usgredg2v  29310  fusgrfis  29413  nbuhgr2vtx1edgblem  29434  nb3grprlem1  29463  cusgrsize2inds  29537  cusgrfi  29542  fusgrn0degnn0  29583  uspgrloopvtxel  29600  vtxdginducedm1lem4  29626  uhgr0edg0rgrb  29658  wlkl1loop  29721  wlk1walk  29722  upgriswlk  29724  upgrwlkvtxedg  29728  uspgr2wlkeq  29729  wlkv0  29733  wlksoneq1eq2  29746  wlkon2n0  29748  wlkreslem  29751  wlkres  29752  lfgrwlkprop  29769  pthdivtx  29810  2pthnloop  29814  spthonepeq  29835  uhgrwkspthlem2  29837  uhgrwkspth  29838  usgr2wlkneq  29839  usgr2trlncl  29843  usgr2pthlem  29846  usgr2pth  29847  cyclnspth  29884  lfgrn1cycl  29888  usgr2trlncrct  29889  uspgrn2crct  29891  crctcshwlkn0lem3  29895  crctcshwlkn0lem5  29897  wwlknp  29926  wspthneq1eq2  29943  0enwwlksnge1  29947  wlklnwwlkln1  29951  wlkiswwlks2  29958  wlkiswwlksupgr2  29960  wlklnwwlkln2lem  29965  wwlksnred  29975  wwlksnextbi  29977  wwlksnredwwlkn0  29979  wwlksnextwrd  29980  wwlksnextinj  29982  wwlksnextproplem3  29994  wwlksnextprop  29995  wspthsnwspthsnon  29999  wspthsnonn0vne  30000  2pthon3v  30026  umgr2adedgwlkonALT  30030  umgr2wlk  30032  umgr2wlkon  30033  usgrwwlks2on  30041  umgrwwlks2on  30042  elwspths2on  30045  elwspths2onw  30046  usgr2wspthons3  30050  elwwlks2  30052  rusgrnumwwlk  30061  clwwlkccatlem  30074  clwlkclwwlklem2a4  30082  clwlkclwwlklem2a  30083  clwlkclwwlklem2  30085  clwlkclwwlkf1lem3  30091  erclwwlkeqlen  30104  clwwlknwwlksn  30123  loopclwwlkn1b  30127  clwwlkf1  30134  wwlksext2clwwlk  30142  eleclclwwlknlem2  30146  umgr2cwwk2dif  30149  eleclclwwlkn  30161  hashecclwwlkn1  30162  umgrhashecclwwlk  30163  clwwlknonwwlknonb  30191  clwwlknonex2lem2  30193  clwwlknonex2  30194  1pthon2v  30238  upgr3v3e3cycl  30265  uhgr3cyclexlem  30266  uhgr3cyclex  30267  eupth2lem3lem4  30316  frgr3vlem1  30358  frgr3vlem2  30359  3vfriswmgrlem  30362  3vfriswmgr  30363  3cyclfrgrrn1  30370  n4cyclfrgr  30376  frgrncvvdeqlem3  30386  frgrncvvdeqlem6  30389  frgrncvvdeqlem7  30390  frgrncvvdeqlem8  30391  frgrwopreglem4a  30395  frgrwopreglem3  30399  frgrwopreg1  30403  frgrwopreg2  30404  frgrwopreglem5lem  30405  frgrwopreglem5ALT  30407  frgrwopreg  30408  fusgr2wsp2nb  30419  2wspmdisj  30422  numclwwlk1lem2foa  30439  numclwwlk1lem2f1  30442  numclwwlk1lem2fo  30443  numclwwlk1  30446  wlkl0  30452  numclwwlk2lem1  30461  numclwlk2lem2f  30462  numclwlk2lem2f1o  30464  frgrreg  30479  frgrregord013  30480  frgrregord13  30481  friendshipgt3  30483  friendship  30484  eulplig  30571  ipassi  30927  ubthlem2  30957  isch3  31327  shintcli  31415  shmodsi  31475  spansncvi  31738  hoaddsub  31902  eigorthi  31923  pjss2coi  32250  pjnormssi  32254  pj3cor1i  32295  strb  32344  dmdmd  32386  mdsl0  32396  csmdsymi  32420  chrelat2i  32451  mdsymlem3  32491  mdsymlem6  32494  sumdmdlem2  32505  opreu2reuALT  32561  ssrelf  32703  gsumwun  33152  r1filim  35263  trssfir1om  35271  fineqvinfep  35285  trssfir1omregs  35296  onvf1odlem4  35304  spthcycl  35327  loop1cycl  35335  cvmlift2lem1  35500  satfrel  35565  satfrnmapom  35568  fmlafvel  35583  fmla1  35585  gonarlem  35592  gonar  35593  goalrlem  35594  goalr  35595  satffunlem  35599  satffunlem1lem1  35600  satffunlem2lem1  35602  satffun  35607  satefvfmla1  35623  mrsubvrs  35720  mclsax  35767  3ccased  35917  dfon2lem3  35981  rdgprc  35990  cgrextend  36206  btwndiff  36225  btwnconn1lem12  36296  brsegle  36306  broutsideof2  36320  funray  36338  in-ax8  36422  ss-ax8  36423  elicc3  36515  nn0prpwlem  36520  nn0prpw  36521  fnessref  36555  neibastop2lem  36558  filnetlem4  36579  meran1  36609  waj-ax  36612  arg-ax  36614  axtco1from2  36673  dfttc4  36728  mh-inf3f1  36739  mh-regprimbi  36743  bj-nnclavc  36824  bj-con2com  36841  bj-axdd2  36873  bj-alrimg  36894  bj-exlimg  36916  bj-exalimi  36926  bj-eximcom  36927  bj-ssbid1ALT  36975  bj-sb  37000  bj-snsetex  37286  bj-axseprep  37397  bj-axreprepsep  37398  bj-restpw  37420  bj-finsumval0  37615  mptsnunlem  37668  icoreclin  37687  relowlpssretop  37694  inunissunidif  37705  rdgssun  37708  finorwe  37712  domalom  37734  wl-dral1d  37870  wl-exeq  37873  wl-lem-exsb  37905  wl-eujustlem1  37927  poimirlem29  37984  poimirlem32  37987  fdc  38080  seqpo  38082  incsequz  38083  isismty  38136  ismtybndlem  38141  heibor1lem  38144  ismgmOLD  38185  isexid2  38190  ghomco  38226  pridlc  38406  relcnveq3  38662  elrelscnveq3  38962  cdleme18d  40755  tendovalco  41225  cdlemn11pre  41670  dihord2pre  41685  indstrd  42646  unitscyglem3  42650  eu6w  43123  incssnn0  43157  fphpd  43262  jm2.19lem3  43437  setindtr  43470  islssfg2  43517  mpaaeu  43596  ordnexbtwnsuc  43713  oaabsb  43740  succlg  43774  oacl2g  43776  omabs2  43778  omcl2  43779  omcl3g  43780  pr2cv  43993  refimssco  44052  iunrelexpmin1  44153  iunrelexpmin2  44157  trclimalb2  44171  clsk1indlem3  44488  tfindsd  44655  mnurndlem1  44726  nzss  44762  sb5ALT  44970  truniALT  44986  ee223  45079  3orbi123VD  45294  sbc3orgVD  45295  exbirVD  45297  exbiriVD  45298  sbcim2gVD  45319  trsbcVD  45321  truniALTVD  45322  onfrALTlem3VD  45331  onfrALTlem2VD  45333  csbrngVD  45340  19.41rgVD  45346  ax6e2eqVD  45351  ax6e2ndeqVD  45353  2uasbanhVD  45355  sb5ALTVD  45357  vk15.4jVD  45358  infxrunb3rnmpt  45874  stoweidlem26  46472  et-equeucl  47318  hirstL-ax3  47352  rexsb  47559  rexrsb  47560  euoreqb  47569  2reu8i  47573  afvres  47632  tz6.12-afv  47633  afvco2  47636  afv2orxorb  47688  afv2res  47699  tz6.12-afv2  47700  tz6.12i-afv2  47703  dfatcolem  47715  zm1nn  47762  2ffzoeq  47788  smonoord  47837  iccpartiltu  47894  iccpartlt  47896  iccpartltu  47897  iccpartgtl  47898  iccpartgt  47899  iccpartleu  47900  iccpartgel  47901  icceuelpart  47908  iccpartnel  47910  lswn0  47916  ichnreuop  47944  ichreuopeq  47945  prsprel  47959  sprsymrelfvlem  47962  sprsymrelf1lem  47963  sprsymrelfolem2  47965  prproropf1olem4  47978  paireqne  47983  prprelb  47988  reupr  47994  goldbachth  48022  odz2prm2pw  48038  fmtno4prmfac  48047  fmtno4prmfac193  48048  prmdvdsfmtnof1lem2  48060  2pwp1prmfmtno  48065  lighneallem2  48081  lighneallem4b  48084  lighneallem4  48085  requad2  48111  odd2prm2  48206  mogoldbblem  48208  gbepos  48246  gbowgt5  48250  gbowge7  48251  stgoldbwt  48264  sbgoldbwt  48265  sbgoldbst  48266  sbgoldbaltlem1  48267  sbgoldbalt  48269  sbgoldbo  48275  nnsum3primesle9  48282  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  bgoldbtbndlem1  48293  bgoldbtbndlem2  48294  bgoldbtbndlem3  48295  bgoldbtbnd  48297  dfnbgr6  48345  isuspgrimlem  48383  uhgrimisgrgric  48419  clnbgrgrim  48422  usgrgrtrirex  48438  isubgr3stgrlem4  48457  grilcbri2  48499  grlicsym  48501  grlictr  48503  gricgrlic  48506  gpgvtxedg0  48551  gpgvtxedg1  48552  gpgedg2ov  48554  gpgedg2iv  48555  pgnioedg1  48596  pgnioedg2  48597  pgnioedg3  48598  pgnioedg4  48599  pgnioedg5  48600  pgnbgreunbgrlem2lem3  48604  pgnbgreunbgrlem3  48606  pgnbgreunbgrlem5lem1  48608  pgnbgreunbgrlem5lem2  48609  pgnbgreunbgrlem5lem3  48610  pgnbgreunbgrlem6  48612  upgrwlkupwlk  48628  uspgrsprf1  48635  lmod0rng  48717  lidldomn1  48719  rngccatidALTV  48760  rngcinvALTV  48764  rhmsubcALTVlem4  48772  funcringcsetcALTV2lem9  48786  ringccatidALTV  48794  ringcbasbasALTV  48800  ztprmneprm  48835  pgrpgt2nabl  48854  lmodvsmdi  48867  ply1mulgsumlem2  48875  lincsumcl  48919  ellcoellss  48923  linindslinci  48936  islinindfis  48937  lincext3  48944  lindslinindimp2lem4  48949  lindslinindsimp2lem5  48950  lindslinindsimp2  48951  lindsrng01  48956  ldepspr  48961  lincresunit3lem1  48967  elfzolborelfzop1  49007  dignn0ldlem  49090  nn0sumshdiglem1  49109  1arymaptf1  49130  2arymaptf1  49141  rrx2xpref1o  49206  rrx2plord2  49210  rrx2plordisom  49211  line2ylem  49239  line2xlem  49241  line2y  49243  itschlc0xyqsol1  49254  inlinecirc02plem  49274  fullthinc  49937  tfis2d  50167  onsetrec  50195