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  158  expt  180  jad  190  pm2.61  195  syl5ibcom  248  syl5ibrcom  250  pm5.501  370  impcom  411  impd  414  expcom  417  expdcom  418  simplbi2com  506  imdistanri  573  jaod  856  orel1  886  pm2.62  897  pm2.75  931  pm2.64  939  ccased  1034  dedlem0b  1040  3impd  1345  3expd  1350  mp3an1i  1451  norassOLD  1535  minimp  1623  meredith  1643  19.35  1878  speimfw  1966  equtrr  2029  equeucl  2031  sb56OLD  2275  sbiedw  2323  sbiedwOLD  2324  cbv1v  2345  exsb  2367  cbv1  2411  ax12b  2435  axc11n  2437  dvelimdf  2460  equvel  2468  dfsb1  2499  sbied  2522  sbequ2ALT  2556  sbiedALT  2590  dfmoeu  2594  mo3  2623  mo4  2625  2mo  2710  2eu6  2719  exists2  2724  rexlimdv  3242  r19.12  3283  r19.35  3295  2gencl  3482  3gencl  3483  vtocl2ga  3523  rspccv  3568  ceqex  3593  mob  3656  euind  3663  reuind  3692  2reu1  3826  sseq2  3941  nelss  3978  rexdifi  4073  reupick2  4241  rspn0OLD  4267  disjeq0  4363  uneqdifeq  4396  sspw  4510  ssprsseq  4718  preq12b  4741  prnebg  4746  prel12g  4754  3elpr2eq  4799  iinss2  4944  trintss  5153  dtru  5236  reusv2lem1  5264  alxfr  5273  ralxfrALT  5281  copsexgw  5346  copsexg  5347  snopeqop  5361  propeqop  5362  opthhausdorff  5372  opthhausdorff0  5373  pocl  5445  pofun  5455  solin  5462  frss  5486  2optocl  5610  3optocl  5611  ssrel  5621  ssrel2  5623  ssrelrel  5633  relop  5685  dfres3  5823  asymref2  5944  xpidtr  5949  trin2  5950  poltletr  5959  xp11  5999  relcnvtrg  6086  reuop  6112  tz7.7  6185  ordtr2  6203  suc11  6262  iotaval  6298  funmo  6340  fundif  6373  fss  6501  f0dom0  6537  fv3  6663  tz6.12i  6671  mpteqb  6764  fveqdmss  6823  eldmrexrnb  6835  funopsn  6887  funsndifnop  6890  tpres  6940  funfvima  6970  fvclss  6979  f1veqaeq  6993  isoselem  7073  oprabv  7193  ovg  7293  elovmpt3rab1  7385  sorpsscmpl  7440  iunpw  7473  ordom  7569  limom  7575  peano5  7585  fornex  7639  funelss  7728  funeldmdif  7729  bropopvvv  7768  bropfvvvvlem  7769  f1o2ndf1  7801  poxp  7805  soxp  7806  suppimacnv  7824  ressuppss  7832  ressuppssdif  7834  tposfn2  7897  wfr3g  7936  onnseq  7964  smoel  7980  smogt  7987  smoiso2  7989  tfr3  8018  tz7.48-2  8061  tz7.48-3  8063  tz7.49  8064  oecl  8145  oaordex  8167  oalimcl  8169  oaass  8170  omordi  8175  omlimcl  8187  odi  8188  omeulem1  8191  oen0  8195  nnawordi  8230  nnaass  8231  nnmordi  8240  omabs  8257  omsmolem  8263  iiner  8352  2ecoptocl  8371  3ecoptocl  8372  undifixp  8481  xpdom2  8595  xpf1o  8663  infensuc  8679  php  8685  onomeneq  8693  isinf  8715  findcard2  8742  unblem2  8755  infssuni  8799  finsschain  8815  fsuppunfi  8837  fsuppunbi  8838  marypha1  8882  hartogs  8992  card2on  9002  card2inf  9003  xpwdomg  9033  elirrv  9044  en3lp  9061  preleqg  9062  inf3lem1  9075  inf3lem2  9076  inf3lem3  9077  inf3lem5  9079  noinfep  9107  trcl  9154  tcel  9171  rankonidlem  9241  scottex  9298  djuunxp  9334  eldju2ndl  9337  updjud  9347  dif1card  9421  fodomnum  9468  cardaleph  9500  kmlem9  9569  kmlem13  9573  cflim2  9674  cfsmolem  9681  infpssrlem3  9716  isfin7-2  9807  fin1a2lem6  9816  fin1a2lem12  9822  domtriomlem  9853  axdc3lem4  9864  axdc4lem  9866  zorn2lem3  9909  zorn2lem4  9910  zorn2lem5  9911  zorn2lem7  9913  zornn0g  9916  axdclem2  9931  ondomon  9974  alephval2  9983  cfpwsdom  9995  wuncval2  10158  grupr  10208  gruiun  10210  ingru  10226  grothomex  10240  indpi  10318  nqereu  10340  prlem934  10444  reclem2pr  10459  mulgt0sr  10516  supsrlem  10522  dedekind  10792  lemul1a  11483  squeeze0  11532  peano5nni  11628  nnunb  11881  nn0lt2  12033  nn0le2is012  12034  fzind  12068  nn0ind-raph  12070  zindd  12071  eluzadd  12261  uzin  12266  nn01to3  12329  xnn0xadd0  12628  xmulasslem  12666  icoshft  12851  fzen  12919  uzsubsubfz  12924  elfz0ubfz0  13006  elfz0fzfz0  13007  fz0fzelfz0  13008  elfzmlbp  13013  elfzodifsumelfzo  13098  ssfzo12bi  13127  elfzonelfzo  13134  elfznelfzo  13137  injresinjlem  13152  injresinj  13153  modfzo0difsn  13306  modsumfzodifsn  13307  addmodlteq  13309  ssnn0fi  13348  fsuppmapnn0fiub0  13356  expcllem  13436  expeq0  13455  mulexp  13464  leexp2r  13534  bernneq  13586  facdiv  13643  hasheqf1oi  13708  hashnn0n0nn  13748  hashss  13766  hashgt12el  13779  hashgt12el2  13780  hashimarni  13798  hashle2pr  13831  pr2pwpr  13833  hashge2el2dif  13834  hashge2el2difr  13835  hashtpg  13839  hashge3el3dif  13840  exprelprel  13843  hash1to3  13845  fundmge2nop0  13846  fi1uzind  13851  ccatsymb  13927  swrdnd  14007  swrdnd2  14008  swrdnnn0nd  14009  swrdnd0  14010  pfxnd0  14041  swrdswrdlem  14057  swrdswrd  14058  pfxccatin12lem2a  14080  pfxccatin12lem1  14081  swrdccatin2  14082  pfxccatin12lem2  14084  pfxccatin12lem3  14085  pfxccat3  14087  swrdccat  14088  swrdccat3blem  14092  repsdf2  14131  repswswrd  14137  cshwidxmod  14156  cshwidx0  14159  cshf1  14163  cshweqrep  14174  cshw1  14175  cshwsexa  14177  2cshwcshw  14178  scshwfzeqfzo  14179  cshwcsh2id  14181  wwlktovfo  14313  relexpaddg  14404  iseraltlem2  15031  modfsummods  15140  clim2prod  15236  prodfn0  15242  prodfrec  15243  prodmo  15282  fprodabs  15320  binomfallfac  15387  fprodefsum  15440  dvdsaddre2b  15649  addmodlteqALT  15667  oddge22np1  15690  nn0enne  15718  nn0o1gt2  15722  sumeven  15728  sumodd  15729  dvdslegcd  15843  gcdneg  15860  dfgcd2  15884  rplpwr  15897  lcmf  15967  lcmftp  15970  lcmfunsnlem2lem1  15972  lcmfunsnlem2  15974  lcmfdvdsb  15977  coprmdvds1  15986  qredeq  15991  coprmprod  15995  coprmproddvdslem  15996  cncongr1  16001  cncongr2  16002  prm2orodd  16025  2mulprm  16027  nnnn0modprm0  16133  prm23lt5  16141  prm23ge5  16142  dvdsprmpweqnn  16211  dvdsprmpweqle  16212  oddprmdvds  16229  prmpwdvds  16230  prmreclem4  16245  ramcl  16355  prmgaplem6  16382  prmgaplem7  16383  prmgaplem8  16384  cshwshashlem1  16421  cshwshashlem2  16422  cshwshashlem3  16423  cshwrepswhash1  16428  setsn0fun  16512  setsstruct2  16513  imasleval  16806  mreiincl  16859  mreexexd  16911  inveq  17036  cicsym  17066  cictr  17067  initoid  17257  termoid  17258  initoeu2lem0  17265  initoeu2lem1  17266  initoeu2lem2  17267  initoeu2  17268  fthestrcsetc  17392  fthsetcestrc  17407  drsdirfi  17540  isnmgm  17848  sgrpass  17899  insubm  17975  mgm2nsgrplem3  18077  dfgrp3lem  18189  cyccom  18338  symg2bas  18513  symgfix2  18536  symgextf1  18541  gsmsymgrfix  18548  pmtrprfv3  18574  psgnunilem4  18617  efgi2  18843  0ringnnzr  20035  psgndiflemB  20289  psgndiflemA  20290  elfrlmbasn0  20452  lmictra  20534  mpfrcl  20757  gsummoncoe1  20933  mamufacex  20996  matecl  21030  dmatelnd  21101  dmatscmcl  21108  scmateALT  21117  scmatsgrp1  21127  scmatf1  21136  mavmulsolcl  21156  cramerimplem1  21288  cramerimplem2  21289  pmatcollpw3fi1  21393  mp2pm2mplem4  21414  pm2mpfo  21419  chmaidscmat  21453  fvmptnn04ifb  21456  chfacfscmul0  21463  chfacfpmmul0  21467  cayhamlem1  21471  cayhamlem3  21492  cayleyhamilton1  21497  fiinopn  21506  tgcl  21574  distop  21600  isclo2  21693  iscldtop  21700  ssnei2  21721  opnnei  21725  pnfnei  21825  mnfnei  21826  tgcnp  21858  cnpnei  21869  1stcelcls  22066  txcnpi  22213  cnmptcom  22283  fbfinnfr  22446  isfildlem  22462  snfil  22469  fbunfip  22474  fgcl  22483  elfm2  22553  fmco  22566  fbflim2  22582  cnpflf2  22605  flimfcls  22631  tmdgsum  22700  neibl  23108  tngngpim  23265  fgcfil  23875  caubl  23912  volsuplem  24159  ellimc3  24482  dvnadd  24532  dvnres  24534  cpnord  24538  dvnfre  24555  ply1divex  24737  cxpmul2  25280  zabsle1  25880  gausslemma2dlem1a  25949  gausslemma2dlem3  25952  lgsquad2lem2  25969  2lgs  25991  2sq2  26017  2sqnn0  26022  2sqnn  26023  2sqreultlem  26031  2sqreunnltlem  26034  qabvexp  26210  axcontlem4  26761  umgredgprv  26900  umgrnloop  26901  upgrpredgv  26932  upgredgpr  26935  edglnl  26936  usgredgprvALT  26985  usgrnloopALT  26993  usgredg2v  27017  fusgrfis  27120  nbuhgr2vtx1edgblem  27141  nb3grprlem1  27170  cusgrsize2inds  27243  cusgrfi  27248  fusgrn0degnn0  27289  uspgrloopvtxel  27306  vtxdginducedm1lem4  27332  uhgr0edg0rgrb  27364  wlkl1loop  27427  wlk1walk  27428  upgriswlk  27430  upgrwlkvtxedg  27434  uspgr2wlkeq  27435  wlkv0  27440  wlklenvclwlkOLD  27445  wlksoneq1eq2  27454  wlkon2n0  27456  wlkreslem  27459  wlkres  27460  lfgrwlkprop  27477  pthdivtx  27518  2pthnloop  27520  spthonepeq  27541  uhgrwkspthlem2  27543  uhgrwkspth  27544  usgr2wlkneq  27545  usgr2trlncl  27549  usgr2pthlem  27552  usgr2pth  27553  cyclnspth  27589  lfgrn1cycl  27591  usgr2trlncrct  27592  uspgrn2crct  27594  crctcshwlkn0lem3  27598  crctcshwlkn0lem5  27600  wwlknp  27629  wspthneq1eq2  27646  0enwwlksnge1  27650  wlklnwwlkln1  27654  wlkiswwlks2  27661  wlkiswwlksupgr2  27663  wlklnwwlkln2lem  27668  wwlksnred  27678  wwlksnextbi  27680  wwlksnredwwlkn0  27682  wwlksnextwrd  27683  wwlksnextinj  27685  wwlksnextproplem3  27697  wwlksnextprop  27698  wspthsnwspthsnon  27702  wspthsnonn0vne  27703  2pthon3v  27729  umgr2adedgwlkonALT  27733  umgr2wlk  27735  umgr2wlkon  27736  umgrwwlks2on  27743  elwspths2on  27746  usgr2wspthons3  27750  elwwlks2  27752  rusgrnumwwlk  27761  clwwlkccatlem  27774  clwlkclwwlklem2a4  27782  clwlkclwwlklem2a  27783  clwlkclwwlklem2  27785  clwlkclwwlkf1lem3  27791  erclwwlkeqlen  27804  clwwlknwwlksn  27823  loopclwwlkn1b  27827  clwwlkf1  27834  wwlksext2clwwlk  27842  eleclclwwlknlem2  27846  umgr2cwwk2dif  27849  eleclclwwlkn  27861  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  clwwlknonwwlknonb  27891  clwwlknonex2lem2  27893  clwwlknonex2  27894  1pthon2v  27938  upgr3v3e3cycl  27965  uhgr3cyclexlem  27966  uhgr3cyclex  27967  eupth2lem3lem4  28016  frgr3vlem1  28058  frgr3vlem2  28059  3vfriswmgrlem  28062  3vfriswmgr  28063  3cyclfrgrrn1  28070  n4cyclfrgr  28076  frgrncvvdeqlem3  28086  frgrncvvdeqlem6  28089  frgrncvvdeqlem7  28090  frgrncvvdeqlem8  28091  frgrwopreglem4a  28095  frgrwopreglem3  28099  frgrwopreg1  28103  frgrwopreg2  28104  frgrwopreglem5lem  28105  frgrwopreglem5ALT  28107  frgrwopreg  28108  fusgr2wsp2nb  28119  2wspmdisj  28122  numclwwlk1lem2foa  28139  numclwwlk1lem2f1  28142  numclwwlk1lem2fo  28143  numclwwlk1  28146  wlkl0  28152  numclwwlk2lem1  28161  numclwlk2lem2f  28162  numclwlk2lem2f1o  28164  frgrreg  28179  frgrregord013  28180  frgrregord13  28181  friendshipgt3  28183  friendship  28184  eulplig  28268  ipassi  28624  ubthlem2  28654  isch3  29024  shintcli  29112  shmodsi  29172  spansncvi  29435  hoaddsub  29599  eigorthi  29620  pjss2coi  29947  pjnormssi  29951  pj3cor1i  29992  strb  30041  dmdmd  30083  mdsl0  30093  csmdsymi  30117  chrelat2i  30148  mdsymlem3  30188  mdsymlem6  30191  sumdmdlem2  30202  opreu2reuALT  30247  ssrelf  30379  spthcycl  32489  loop1cycl  32497  cvmlift2lem1  32662  satfrel  32727  satfrnmapom  32730  fmlafvel  32745  fmla1  32747  gonarlem  32754  gonar  32755  goalrlem  32756  goalr  32757  satffunlem  32761  satffunlem1lem1  32762  satffunlem2lem1  32764  satffun  32769  satefvfmla1  32785  mrsubvrs  32882  mclsax  32929  3ccased  33062  dfon2lem3  33143  rdgprc  33152  trpredmintr  33183  trpredrec  33190  frr3g  33234  sltval2  33276  nolt02o  33312  sslttr  33381  scutun12  33384  cgrextend  33582  btwndiff  33601  btwnconn1lem12  33672  brsegle  33682  broutsideof2  33696  funray  33714  elicc3  33778  nn0prpwlem  33783  nn0prpw  33784  fnessref  33818  neibastop2lem  33821  filnetlem4  33842  meran1  33872  waj-ax  33875  arg-ax  33877  bj-con2com  34009  bj-axdd2  34039  bj-alrimg  34065  bj-exlimg  34069  bj-exalimi  34079  bj-cbvalimt  34085  bj-eximcom  34089  bj-ssbid1ALT  34111  bj-sb  34134  bj-dtru  34254  bj-snsetex  34399  bj-restpw  34507  bj-finsumval0  34700  mptsnunlem  34755  icoreclin  34774  relowlpssretop  34781  inunissunidif  34792  rdgssun  34795  finorwe  34799  domalom  34821  wl-dral1d  34936  wl-exeq  34939  wl-lem-exsb  34967  poimirlem29  35086  poimirlem32  35089  fdc  35183  seqpo  35185  incsequz  35186  isismty  35239  ismtybndlem  35244  heibor1lem  35247  ismgmOLD  35288  isexid2  35293  ghomco  35329  pridlc  35509  relcnveq3  35738  elrelscnveq3  35891  cdleme18d  37591  tendovalco  38061  cdlemn11pre  38506  dihord2pre  38521  nnadddir  39471  incssnn0  39652  fphpd  39757  jm2.19lem3  39932  setindtr  39965  islssfg2  40015  mpaaeu  40094  pr2cv  40247  refimssco  40307  iunrelexpmin1  40409  iunrelexpmin2  40413  trclimalb2  40427  clsk1indlem3  40746  syldbl2  40872  tfindsd  40918  mnurndlem1  40989  nzss  41021  sb5ALT  41231  truniALT  41247  ee223  41340  3orbi123VD  41556  sbc3orgVD  41557  exbirVD  41559  exbiriVD  41560  sbcim2gVD  41581  trsbcVD  41583  truniALTVD  41584  onfrALTlem3VD  41593  onfrALTlem2VD  41595  csbrngVD  41602  19.41rgVD  41608  ax6e2eqVD  41613  ax6e2ndeqVD  41615  2uasbanhVD  41617  sb5ALTVD  41619  vk15.4jVD  41620  infxrunb3rnmpt  42065  stoweidlem26  42668  hirstL-ax3  43485  rexsb  43654  rexrsb  43655  euoreqb  43665  2reu8i  43669  afvres  43728  tz6.12-afv  43729  afvco2  43732  afv2orxorb  43784  afv2res  43795  tz6.12-afv2  43796  tz6.12i-afv2  43799  dfatcolem  43811  zm1nn  43859  fzoopth  43884  2ffzoeq  43885  smonoord  43888  iccpartiltu  43939  iccpartlt  43941  iccpartltu  43942  iccpartgtl  43943  iccpartgt  43944  iccpartleu  43945  iccpartgel  43946  icceuelpart  43953  iccpartnel  43955  lswn0  43961  ichnreuop  43989  ichreuopeq  43990  prsprel  44004  sprsymrelfvlem  44007  sprsymrelf1lem  44008  sprsymrelfolem2  44010  prproropf1olem4  44023  paireqne  44028  prprelb  44033  reupr  44039  goldbachth  44064  odz2prm2pw  44080  fmtno4prmfac  44089  fmtno4prmfac193  44090  prmdvdsfmtnof1lem2  44102  2pwp1prmfmtno  44107  lighneallem2  44124  lighneallem4b  44127  lighneallem4  44128  requad2  44141  odd2prm2  44236  mogoldbblem  44238  gbepos  44276  gbowgt5  44280  gbowge7  44281  stgoldbwt  44294  sbgoldbwt  44295  sbgoldbst  44296  sbgoldbaltlem1  44297  sbgoldbalt  44299  sbgoldbo  44305  nnsum3primesle9  44312  nnsum4primesodd  44314  nnsum4primesoddALTV  44315  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  bgoldbtbndlem1  44323  bgoldbtbndlem2  44324  bgoldbtbndlem3  44325  bgoldbtbnd  44327  isomuspgrlem1  44345  upgrwlkupwlk  44368  uspgrsprf1  44375  mgmhmlin  44406  issubmgm2  44410  lmod0rng  44492  lidldomn1  44545  lidlmmgm  44549  rnghmsscmap  44598  rnghmsubcsetclem2  44600  rngcinv  44605  rngccatidALTV  44613  rngcinvALTV  44617  funcrngcsetc  44622  funcrngcsetcALT  44623  rhmsscmap  44644  rhmsubcsetclem2  44646  rhmsubcrngclem2  44652  ringcinv  44656  ringcbasbas  44658  funcringcsetc  44659  funcringcsetcALTV2lem9  44668  ringccatidALTV  44676  ringcinvALTV  44680  ringcbasbasALTV  44682  rhmsubclem4  44713  rhmsubcALTVlem4  44731  ztprmneprm  44749  pgrpgt2nabl  44768  lmodvsmdi  44784  ply1mulgsumlem2  44795  lincsumcl  44840  ellcoellss  44844  linindslinci  44857  islinindfis  44858  lincext3  44865  lindslinindimp2lem4  44870  lindslinindsimp2lem5  44871  lindslinindsimp2  44872  lindsrng01  44877  ldepspr  44882  lincresunit3lem1  44888  elfzolborelfzop1  44928  dignn0ldlem  45016  nn0sumshdiglem1  45035  1arymaptf1  45056  2arymaptf1  45067  rrx2xpref1o  45132  rrx2plord2  45136  rrx2plordisom  45137  line2ylem  45165  line2xlem  45167  line2y  45169  itschlc0xyqsol1  45180  inlinecirc02plem  45200  tfis2d  45210  onsetrec  45237