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.24  121  con3rr3  151  expt  168  jad  174  pm2.61  183  syl5ibcom  235  syl5ibrcom  237  pm5.501  356  jaod  395  orel1  397  pm2.62  425  impcom  446  impd  447  expcom  451  expd  452  pm3.21  464  simplbi2com  657  imdistanri  727  pm2.64  830  pm2.75  894  ccased  988  dedlem0b  1001  3impd  1281  3expd  1284  mp3an1i  1417  minimp  1560  meredith  1566  19.35  1805  speimfw  1876  sbequ2  1882  equtrr  1949  equeucl  1951  sb56  2150  axc11nlemOLD  2160  cbv1  2267  axc11nlemALT  2306  axc11n  2307  dvelimdf  2335  ax12b  2345  equvel  2347  sbied  2409  exsb  2468  mo2v  2477  euex  2494  exmoeu  2502  mo3  2507  2mo  2551  2eu6  2558  exists2  2562  rexlimdv  3030  r19.12  3063  2gencl  3236  3gencl  3237  rspccv  3306  ceqex  3333  mob  3388  euind  3393  reuind  3411  sseq2  3627  nelss  3664  reupick2  3913  rspn0  3934  uneqdifeq  4057  uneqdifeqOLD  4058  eqoreldifOLD  4226  ssprsseq  4357  eqsnOLD  4362  preq12b  4382  prel12  4383  prnebg  4389  3elpr2eq  4435  iinss2  4572  disjxiunOLD  4650  trintss  4769  dtru  4857  reusv1OLD  4867  reusv2lem1  4868  alxfr  4878  ralxfrALT  4887  sspwb  4917  copsexg  4956  propeqop  4970  pocl  5042  pofun  5051  solin  5058  frss  5081  2optocl  5196  3optocl  5197  ssrel  5207  ssrelOLD  5208  ssrel2  5210  ssrelrel  5220  relop  5272  dfres3  5403  restidsingOLD  5459  asymref2  5513  xpidtr  5518  trin2  5519  poltletr  5528  xp11  5569  relcnvtr  5655  tz7.7  5749  ordtri3OLD  5760  ordtr2  5768  suc11  5831  iotaval  5862  funmo  5904  fundif  5935  fss  6056  f0dom0  6089  fv3  6206  tz6.12c  6213  tz6.12i  6214  mpteqb  6299  fveqdmss  6354  eldmrexrnb  6366  funopsn  6413  funsndifnop  6416  tpres  6466  funfvima  6492  fvclss  6500  f1veqaeq  6514  isoselem  6591  oprabv  6703  ovg  6799  elovmpt3rab1  6893  sorpsscmpl  6948  iunpw  6978  ordom  7074  limom  7080  peano5  7089  fornex  7135  bropopvvv  7255  bropfvvvvlem  7256  f1o2ndf1  7285  poxp  7289  soxp  7290  suppimacnv  7306  ressuppss  7314  ressuppssdif  7316  tposfn2  7374  wfr3g  7413  onnseq  7441  smoel  7457  smogt  7464  smoiso2  7466  tfr3  7495  tz7.48-2  7537  tz7.48-3  7539  tz7.49  7540  oecl  7617  oaordex  7638  oalimcl  7640  oaass  7641  omordi  7646  omlimcl  7658  odi  7659  omeulem1  7662  oen0  7666  nnawordi  7701  nnaass  7702  nnmordi  7711  omabs  7727  omsmolem  7733  iiner  7819  2ecoptocl  7838  3ecoptocl  7839  undifixp  7944  xpdom2  8055  xpf1o  8122  infensuc  8138  php  8144  onomeneq  8150  isinf  8173  findcard2  8200  unblem2  8213  infssuni  8257  finsschain  8273  fsuppunfi  8295  fsuppunbi  8296  marypha1  8340  hartogs  8449  card2on  8459  card2inf  8460  xpwdomg  8490  elirrv  8504  en3lp  8513  inf3lem1  8525  inf3lem2  8526  inf3lem3  8527  inf3lem5  8529  noinfep  8557  trcl  8604  tcel  8621  rankonidlem  8691  scottex  8748  dif1card  8833  fodomnum  8880  cardaleph  8912  kmlem9  8980  kmlem13  8984  cflim2  9085  cfsmolem  9092  infpssrlem3  9127  isfin7-2  9218  fin1a2lem6  9227  fin1a2lem10  9231  fin1a2lem12  9233  domtriomlem  9264  axdc3lem4  9275  axdc4lem  9277  zorn2lem3  9320  zorn2lem4  9321  zorn2lem5  9322  zorn2lem7  9324  zornn0g  9327  axdclem2  9342  ondomon  9385  alephval2  9394  cfpwsdom  9406  wuncval2  9569  grupr  9619  gruiun  9621  ingru  9637  grothomex  9651  indpi  9729  nqereu  9751  prlem934  9855  reclem2pr  9870  mulgt0sr  9926  supsrlem  9932  dedekind  10200  lemul1a  10877  squeeze0  10926  peano5nni  11023  nnunb  11288  nn0lt2  11440  nn0le2is012  11441  fzind  11475  nn0ind-raph  11477  zindd  11478  eluzadd  11716  uzin  11720  nn01to3  11781  xnn0xadd0  12077  xmulasslem  12115  icoshft  12294  fzen  12358  uzsubsubfz  12363  elfz0ubfz0  12443  elfz0fzfz0  12444  fz0fzelfz0  12445  elfzmlbp  12450  elfzodifsumelfzo  12533  ssfzo12bi  12563  elfzonelfzo  12570  elfznelfzo  12573  injresinjlem  12588  injresinj  12589  modfzo0difsn  12742  modsumfzodifsn  12743  addmodlteq  12745  ssnn0fi  12784  fsuppmapnn0fiub0  12793  expcllem  12871  expeq0  12890  mulexp  12899  leexp2r  12918  bernneq  12990  facdiv  13074  hasheqf1oi  13140  hasheqf1oiOLD  13141  hashf1rnOLD  13143  hashnn0n0nn  13180  hashss  13197  hashgt12el  13210  hashgt12el2  13211  hashmap  13222  hashimarni  13228  hash2prde  13252  hashle2pr  13259  pr2pwpr  13261  hashge2el2dif  13262  hashge2el2difr  13263  hashtpg  13267  hashge3el3dif  13268  exprelprel  13271  hash1to3  13273  fundmge2nop0  13274  fi1uzind  13279  fi1uzindOLD  13285  ccatsymb  13366  swrdnd  13432  swrdnd2  13433  swrdswrdlem  13459  swrdswrd  13460  swrdccatin1  13483  swrdccatin12lem2a  13485  swrdccatin12lem2b  13486  swrdccatin2  13487  swrdccatin12lem2  13489  swrdccatin12lem3  13490  swrdccat3  13492  swrdccat  13493  swrdccat3blem  13495  repsdf2  13525  repswswrd  13531  cshwidxmod  13549  cshwidx0  13552  cshf1  13556  2cshw  13559  cshweqrep  13567  cshw1  13568  cshwsexa  13570  2cshwcshw  13571  scshwfzeqfzo  13572  cshwcsh2id  13574  swrdco  13583  wwlktovfo  13701  relexpaddg  13793  cjexp  13890  absexp  14044  iseraltlem2  14413  modfsummods  14525  clim2prod  14620  prodfn0  14626  prodfrec  14627  prodmo  14666  fprodabs  14704  binomfallfac  14772  fprodefsum  14825  dvdsaddre2b  15029  addmodlteqALT  15047  oddge22np1  15073  nn0enne  15094  nn0o1gt2  15097  sumeven  15110  sumodd  15111  dvdslegcd  15226  gcdneg  15243  dfgcd2  15263  rplpwr  15276  lcmf  15346  lcmftp  15349  lcmfunsnlem2lem1  15351  lcmfunsnlem2  15353  lcmfdvds  15355  lcmfdvdsb  15356  lcmfunsn  15357  coprmdvds1  15365  qredeq  15371  coprmprod  15375  coprmproddvdslem  15376  cncongr1  15381  cncongr2  15382  prm2orodd  15404  nnnn0modprm0  15511  prm23lt5  15519  prm23ge5  15520  dvdsprmpweqnn  15589  dvdsprmpweqle  15590  oddprmdvds  15607  prmpwdvds  15608  prmreclem4  15623  ramcl  15733  prmgaplem6  15760  prmgaplem7  15761  prmgaplem8  15762  cshwshashlem1  15802  cshwshashlem2  15803  cshwshashlem3  15804  cshwrepswhash1  15809  setsn0fun  15895  setsstruct2  15896  setsstructOLD  15899  imasleval  16201  mreiincl  16256  mreexexd  16308  mreexexdOLD  16309  inveq  16434  cicsym  16464  cictr  16465  initoid  16655  termoid  16656  initoeu2lem0  16663  initoeu2lem1  16664  initoeu2lem2  16665  initoeu2  16666  fthestrcsetc  16790  fthsetcestrc  16805  drsdirfi  16938  isnmgm  17246  sgrpass  17290  mgm2nsgrplem3  17407  dfgrp3lem  17513  symg2bas  17818  symgfix2  17836  symgextf1  17841  gsmsymgrfix  17848  pmtrprfv3  17874  psgnunilem4  17917  efgi2  18138  lmodvsmmulgdi  18898  0ringnnzr  19269  mpfrcl  19518  gsummoncoe1  19674  psgndiflemB  19946  psgndiflemA  19947  elfrlmbasn0  20106  lmictra  20184  mamufacex  20195  matecl  20231  dmatelnd  20302  dmatscmcl  20309  scmateALT  20318  scmatsgrp1  20328  scmatf1  20337  mavmulsolcl  20357  cramerimplem1  20489  cramerimplem2  20490  pmatcollpw3fi1  20593  mp2pm2mplem4  20614  pm2mpfo  20619  chmaidscmat  20653  fvmptnn04ifb  20656  chfacfscmul0  20663  chfacfpmmul0  20667  cayhamlem1  20671  cayhamlem3  20692  cayleyhamilton1  20697  fiinopn  20706  toprntopon  20729  tgcl  20773  distop  20799  isclo2  20892  iscldtop  20899  ssnei2  20920  opnnei  20924  pnfnei  21024  mnfnei  21025  tgcnp  21057  cnpnei  21068  1stcelcls  21264  txcnpi  21411  cnmptcom  21481  fbfinnfr  21645  isfildlem  21661  snfil  21668  fbunfip  21673  fgcl  21682  elfm2  21752  fmco  21765  fbflim2  21781  cnpflf2  21804  flimfcls  21830  tmdgsum  21899  neibl  22306  tngngpim  22463  fgcfil  23069  caubl  23106  volsuplem  23323  ellimc3  23643  dvnadd  23692  dvnres  23694  cpnord  23698  dvnfre  23715  ply1divex  23896  cxpmul2  24435  zabsle1  25021  lgsqrmodndvds  25078  gausslemma2dlem0i  25089  gausslemma2dlem1a  25090  gausslemma2dlem3  25093  lgsquad2lem2  25110  2lgs  25132  qabvexp  25315  axcontlem4  25847  umgredgprv  26002  umgrnloop  26003  upgrpredgv  26034  upgredgpr  26037  edglnl  26038  usgredgprvALT  26087  usgrnloopALT  26095  usgredg2v  26119  fusgrfis  26222  nbuhgr2vtx1edgblem  26247  nb3grprlem1  26282  cusgrsize2inds  26349  cusgrfi  26354  fusgrn0degnn0  26395  uspgrloopvtxel  26412  vtxdginducedm1lem4  26438  uhgr0edg0rgrb  26470  wlkl1loop  26534  wlk1walk  26535  upgriswlk  26537  upgrwlkvtxedg  26541  uspgr2wlkeq  26542  wlkv0  26547  wlklenvclwlk  26551  wlksoneq1eq2  26560  wlkon2n0  26562  wlkreslem  26566  wlkres  26567  lfgrwlkprop  26584  pthdivtx  26625  2pthnloop  26627  spthonepeq  26648  uhgrwkspthlem2  26650  uhgrwkspth  26651  usgr2wlkneq  26652  usgr2trlncl  26656  usgr2pthlem  26659  usgr2pth  26660  cyclnspth  26695  lfgrn1cycl  26697  usgr2trlncrct  26698  uspgrn2crct  26700  crctcshwlkn0lem3  26704  crctcshwlkn0lem5  26706  wwlknp  26734  wspthneq1eq2  26745  0enwwlksnge1  26749  wlklnwwlkln1  26754  wlkiswwlks2  26761  wlkiswwlksupgr2  26763  wlklnwwlkln2lem  26768  wwlksnred  26787  wwlksnext  26788  wwlksnextbi  26789  wwlksnredwwlkn0  26791  wwlksnextwrd  26792  wwlksnextinj  26794  wwlksnextproplem3  26806  wwlksnextprop  26807  wspthsnwspthsnon  26811  wspthsnonn0vne  26813  wspn0  26820  2pthon3v  26839  umgr2adedgwlkonALT  26843  umgr2wlk  26845  umgr2wlkon  26846  elwwlks2ons3  26848  umgrwwlks2on  26850  elwspths2on  26853  usgr2wspthons3  26857  elwwlks2  26861  rusgrnumwwlk  26870  clwwlknclwwlkdifs  26873  clwwlknp  26887  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  clwlkclwwlklem2  26901  clwwlksf1  26917  wwlksext2clwwlk  26924  erclwwlkseqlen  26933  eleclclwwlksnlem2  26939  umgr2cwwk2dif  26941  eleclclwwlksn  26953  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  clwlksfclwwlk  26962  clwlksfoclwwlk  26963  clwwlksnun  26974  1pthon2v  27013  upgr3v3e3cycl  27040  uhgr3cyclexlem  27041  uhgr3cyclex  27042  eupth2lem3lem4  27091  frgr3vlem1  27137  frgr3vlem2  27138  3vfriswmgrlem  27141  3vfriswmgr  27142  3cyclfrgrrn1  27149  n4cyclfrgr  27155  frgrncvvdeqlem3  27165  frgrncvvdeqlem6  27168  frgrncvvdeqlem7  27169  frgrncvvdeqlem8  27170  frgrwopreglem4a  27174  frgrwopreglem3  27178  frgrwopreg1  27182  frgrwopreg2  27183  frgrwopreglem5lem  27184  frgrwopreglem5ALT  27186  frgrwopreg  27187  fusgr2wsp2nb  27198  2wspmdisj  27201  clwwlksnwwlksn  27209  numclwwlkovf2exlem2  27212  numclwwlkovf2ex  27219  numclwlk1lem2foa  27224  numclwlk1lem2f1  27227  numclwlk1lem2fo  27228  numclwwlk1  27231  numclwwlk2lem1  27235  numclwlk2lem2f  27236  numclwlk2lem2f1o  27238  frgrreg  27252  frgrregord013  27253  frgrregord13  27254  friendshipgt3  27256  friendship  27257  eulplig  27337  ipassi  27696  ubthlem2  27727  isch3  28098  shintcli  28188  shmodsi  28248  spansncvi  28511  hoaddsub  28675  eigorthi  28696  pjss2coi  29023  pjnormssi  29027  pj3cor1i  29068  strb  29117  dmdmd  29159  mdsl0  29169  csmdsymi  29193  chrelat2i  29224  mdsymlem3  29264  mdsymlem6  29267  sumdmdlem2  29278  ssrelf  29425  cvmlift2lem1  31284  mrsubvrs  31419  mclsax  31466  3ccased  31600  dfon2lem3  31690  rdgprc  31700  trpredmintr  31731  trpredrec  31738  frr3g  31779  sltval2  31809  nolt02o  31845  sslttr  31914  scutun12  31917  cgrextend  32115  btwndiff  32134  btwnconn1lem12  32205  brsegle  32215  broutsideof2  32229  funray  32247  elicc3  32311  nn0prpwlem  32317  nn0prpw  32318  fnessref  32352  neibastop2lem  32355  filnetlem4  32376  meran1  32410  waj-ax  32413  arg-ax  32415  bj-con2com  32548  bj-axdd2  32576  bj-exalimi  32612  bj-ssbequ2  32643  bj-ssbequ1  32644  bj-ssbid1ALT  32648  bj-sb  32677  bj-cbv1v  32729  bj-dtru  32797  bj-mo3OLD  32832  bj-snsetex  32951  bj-restpw  33045  bj-finsumval0  33147  mptsnunlem  33185  icoreclin  33205  relowlpssretop  33212  wl-dveeq12  33311  wl-dral1d  33318  wl-exeq  33321  wl-lem-exsb  33348  poimirlem29  33438  poimirlem32  33441  fdc  33541  seqpo  33543  incsequz  33544  isismty  33600  ismtybndlem  33605  heibor1lem  33608  ismgmOLD  33649  isexid2  33654  ghomco  33690  pridlc  33870  relcnveq3  34092  cdleme18d  35582  tendovalco  36053  cdlemn11pre  36499  dihord2pre  36514  incssnn0  37274  fphpd  37380  jm2.19lem3  37558  setindtr  37591  islssfg2  37641  mpaaeu  37720  refimssco  37913  iunrelexpmin1  38000  iunrelexpmin2  38004  trclimalb2  38018  clsk1indlem3  38341  syldbl2  38468  nzss  38516  sb5ALT  38731  truniALT  38751  ee223  38859  3orbi123VD  39085  sbc3orgVD  39086  exbirVD  39088  exbiriVD  39089  sbcim2gVD  39111  trsbcVD  39113  truniALTVD  39114  onfrALTlem3VD  39123  onfrALTlem2VD  39125  csbrngVD  39132  19.41rgVD  39138  ax6e2eqVD  39143  ax6e2ndeqVD  39145  2uasbanhVD  39147  sb5ALTVD  39149  vk15.4jVD  39150  infxrunb3rnmpt  39655  stoweidlem26  40243  hirstL-ax3  41059  rexsb  41168  rexrsb  41169  2reu1  41186  afvres  41252  tz6.12-afv  41253  afvco2  41256  zm1nn  41316  fzoopth  41337  2ffzoeq  41338  smonoord  41341  iccpartiltu  41358  iccpartlt  41360  iccpartltu  41361  iccpartgtl  41362  iccpartgt  41363  iccpartleu  41364  iccpartgel  41365  icceuelpart  41372  iccpartnel  41374  lswn0  41380  pfxccatin12lem1  41423  pfxccatin12lem2  41424  pfxccat3  41426  goldbachth  41459  odz2prm2pw  41475  fmtno4prmfac  41484  fmtno4prmfac193  41485  prmdvdsfmtnof1lem2  41497  2pwp1prmfmtno  41504  lighneallem2  41523  lighneallem4b  41526  lighneallem4  41527  odd2prm2  41627  mogoldbblem  41629  gbepos  41646  gbowgt5  41650  gbowge7  41651  stgoldbwt  41664  sbgoldbwt  41665  sbgoldbst  41666  sbgoldbaltlem1  41667  sbgoldbalt  41669  sbgoldbo  41675  nnsum3primesle9  41682  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  bgoldbtbndlem1  41693  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  bgoldbtbnd  41697  upgrwlkupwlk  41721  prsprel  41737  sprsymrelfvlem  41740  sprsymrelf1lem  41741  sprsymrelfolem2  41743  uspgrsprf1  41755  mgmhmlin  41786  issubmgm2  41790  lmod0rng  41868  lidldomn1  41921  lidlmmgm  41925  rnghmsscmap  41974  rnghmsubcsetclem2  41976  rngcinv  41981  rngccatidALTV  41989  rngcinvALTV  41993  funcrngcsetc  41998  funcrngcsetcALT  41999  rhmsscmap  42020  rhmsubcsetclem2  42022  rhmsubcrngclem2  42028  ringcinv  42032  ringcbasbas  42034  funcringcsetc  42035  funcringcsetcALTV2lem9  42044  ringccatidALTV  42052  ringcinvALTV  42056  ringcbasbasALTV  42058  rhmsubclem4  42089  rhmsubcALTVlem4  42107  ztprmneprm  42125  pgrpgt2nabl  42147  lmodvsmdi  42163  ply1mulgsumlem2  42175  lincsumcl  42220  ellcoellss  42224  linindslinci  42237  islinindfis  42238  lincext3  42245  lindslinindimp2lem4  42250  lindslinindsimp2lem5  42251  lindslinindsimp2  42252  lindsrng01  42257  ldepspr  42262  lincresunit3lem1  42268  elfzolborelfzop1  42309  dignn0ldlem  42396  nn0sumshdiglem1  42415  tfis2d  42427  onsetrec  42451