Theorem com12 33

Description: Inference that swaps (commutes) antecedents in an implication. Inference associated with pm2.04 91. Its associated inference is mpi 21. (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 23	. 2 ⊢ (𝜓 → 𝜓)
2		com12.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5com 32	1 ⊢ (𝜓 → (𝜑 → 𝜒))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl11  34  syl5  35  syl6com  38  mpcom  39  syli  40  syl2imc  42  pm2.27  43  syldc  49  pm2.43b  56  syl9r  79  com3r  88  pm2.86i  111  pm2.24  125  con3rr3  156  exptOLD  179  jad  189  pm2.61  194  syl5ibcom  248  syl5ibrcom  250  pm5.501  369  impcom  413  impd  416  expcom  419  expdcom  420  simplbi2com  508  imdistanri  580  syldbl2  855  jaod  873  orel1  902  pm2.62  913  pm2.75  947  pm2.64  956  ccased  1054  dedlem0b  1060  3impd  1367  3expd  1372  mp3an1i  1483  minimp  1654  meredith  1674  19.35  1910  speimfw  1996  equtrr  2055  equeucl  2057  ax12ev2  2219  sbiedw  2352  cbv1v  2371  exsb  2394  cbv1  2437  ax12b  2459  axc11n  2461  dvelimdf  2484  equvel  2491  dfsb1  2516  sbied  2538  dfmoeu  2566  mo3  2595  mo4  2597  2mo  2679  2eu6  2687  exists2  2692  pm2.61dne  3047  rexlimdv  3167  r19.21v  3193  r19.12  3317  2gencl  3500  3gencl  3501  vtocl2ga  3545  vtocl2gaf  3546  vtocl3gaf  3547  vtocl3ga  3548  vtocl4ga  3550  rspccv  3581  ceqex  3614  mob  3683  euind  3690  reuind  3719  2reu1  3854  sseq2  3966  nelss  4006  rexdifi  4107  reupick2  4287  disjeq0  4419  uneqdifeq  4458  sspw  4578  ssprsseq  4796  preq12b  4820  prnebg  4826  prel12g  4834  3elpr2eq  4876  iinss2  5027  trintss  5242  dtruALT2  5346  reusv2lem1  5374  alxfr  5383  ralxfrALT  5391  exexneq  5421  copsexgw  5477  copsexgwOLD  5478  copsexg  5479  snopeqop  5494  propeqop  5495  opthhausdorff  5505  opthhausdorff0  5506  pofun  5592  solin  5601  frss  5630  2optocl  5762  3optocl  5763  ssrel  5774  ssrel2  5776  ssrelrel  5787  relop  5841  dfres3  5988  asymref2  6122  xpidtr  6127  trin2  6128  poltletr  6137  xp11  6178  imadifssranOLD  6208  relcnvtrgOLD  6274  reuop  6301  tz7.7  6393  ordtr2  6413  suc11  6477  fundif  6592  fss  6729  f0dom0  6769  fv3  6906  tz6.12i  6914  mpteqb  7016  fveqdmss  7080  eldmrexrnb  7094  funopsnOLD  7152  funsndifnop  7155  tpres  7206  funfvima  7235  fvclss  7246  f1veqaeq  7261  fvf1pr  7316  isoselem  7350  oprabv  7483  ovg  7588  elovmpt3rab1  7683  sorpsscmpl  7744  iunpw  7779  trom  7880  limom  7887  peano5  7899  focdmex  7962  funelss  8053  funeldmdif  8054  bropopvvv  8094  bropfvvvvlem  8095  f1o2ndf1  8126  poxp  8133  soxp  8134  poxp2  8148  frxp2  8149  frxp3  8156  suppimacnv  8179  ressuppss  8188  ressuppssdif  8190  tposfn2  8253  wfr3g  8325  onnseq  8340  smoel  8356  smogt  8363  smoiso2  8365  tfr3  8395  tz7.48-2  8438  tz7.48-3  8440  tz7.49  8441  oecl  8531  oaordex  8552  oalimcl  8554  oaass  8555  omordi  8560  omlimcl  8572  odi  8573  omeulem1  8576  oen0  8581  nnawordi  8616  nnaass  8617  nnmordi  8626  omabs  8646  omsmolem  8652  naddssim  8681  brinxper  8733  iiner  8796  2ecoptocl  8815  3ecoptocl  8816  undifixp  8941  xpdom2  9070  xpf1o  9137  infensuc  9153  findcard2  9159  php  9201  isinf  9235  unblem2  9263  fodomfir  9297  infssuni  9313  finsschain  9326  fsuppunfi  9358  fsuppunbi  9359  marypha1  9404  hartogs  9516  card2on  9526  card2inf  9527  xpwdomg  9557  elirrvOLD  9570  elirrvOLDOLD  9571  en3lp  9593  preleqg  9594  inf3lem1  9607  inf3lem2  9608  inf3lem3  9609  inf3lem5  9611  noinfep  9639  ttrclss  9699  ttrclselem2  9705  trcl  9707  tcel  9722  frr3g  9738  rankonidlem  9810  scottexOLD  9873  djuunxp  9926  eldju2ndl  9929  updjud  9939  dif1card  10013  fodomnum  10060  cardaleph  10092  kmlem9  10161  kmlem13  10165  cflim2  10265  cfsmolem  10272  infpssrlem3  10307  isfin7-2  10398  fin1a2lem6  10407  fin1a2lem12  10413  domtriomlem  10444  axdc3lem4  10455  axdc4lem  10457  zorn2lem3  10500  zorn2lem4  10501  zorn2lem5  10502  zorn2lem7  10504  zornn0g  10507  axdclem2  10522  ondomon  10565  alephval2  10575  cfpwsdom  10587  wuncval2  10750  grupr  10800  gruiun  10802  ingru  10818  grothomex  10832  indpi  10910  nqereu  10932  prlem934  11036  reclem2pr  11051  mulgt0sr  11108  supsrlem  11114  1re  11226  dedekind  11391  lemul1a  12087  squeeze0  12136  peano5nni  12254  nnadddir  12310  nnunb  12518  nn0lt2  12677  nn0le2is012  12678  fzind  12712  nn0ind-raph  12714  zindd  12715  uzin  12916  nn01to3  12983  xnn0xadd0  13291  xmulasslem  13329  icoshft  13518  fzen  13587  uzsubsubfz  13593  elfz0ubfz0  13679  elfz0fzfz0  13680  fz0fzelfz0  13681  elfzmlbp  13686  elfzodifsumelfzo  13779  ssfzo12bi  13809  fzoopth  13810  elfzonelfzo  13817  elfznelfzo  13821  injresinjlem  13838  injresinj  13839  modfzo0difsn  13999  modsumfzodifsn  14000  addmodlteq  14002  ssnn0fi  14041  fsuppmapnn0fiub0  14049  expcllem  14128  expeq0  14148  mulexp  14157  leexp2r  14230  bernneq  14285  facdiv  14343  hasheqf1oi  14407  hashnn0n0nn  14447  hashss  14465  hashgt12el  14479  hashgt12el2  14480  hashimarni  14498  hashle2pr  14534  pr2pwpr  14536  hashge2el2dif  14537  hashge2el2difr  14538  hashtpg  14542  hashge3el3dif  14544  exprelprel  14547  hash1to3  14549  hash3tpde  14550  tpfo  14557  fundmge2nop0  14559  fi1uzind  14564  ccatsymb  14640  swrdnd  14716  swrdnd2  14717  swrdnnn0nd  14718  swrdnd0  14719  pfxnd0  14750  swrdswrdlem  14765  swrdswrd  14766  pfxccatin12lem2a  14788  pfxccatin12lem1  14789  swrdccatin2  14790  pfxccatin12lem2  14792  pfxccatin12lem3  14793  pfxccat3  14795  swrdccat  14796  swrdccat3blem  14800  repsdf2  14841  repswswrd  14847  cshwidxmod  14866  cshwidx0  14869  cshf1  14873  cshweqrep  14884  cshw1  14885  2cshwcshw  14888  scshwfzeqfzo  14889  cshwcsh2id  14891  wwlktovfo  15021  relexpaddg  15116  iseraltlem2  15760  modfsummods  15871  clim2prod  15968  prodfn0  15974  prodfrec  15975  prodmo  16016  fprodabs  16054  binomfallfac  16120  fprodefsum  16174  dvdsaddre2b  16390  addmodlteqALT  16408  oddge22np1  16432  nn0enne  16460  nn0o1gt2  16464  sumeven  16470  sumodd  16471  dvdslegcd  16587  gcdneg  16605  dfgcd2  16629  rplpwr  16641  lcmf  16716  lcmftp  16719  lcmfunsnlem2lem1  16721  lcmfunsnlem2  16723  lcmfdvdsb  16726  coprmdvds1  16735  qredeq  16740  coprmprod  16744  coprmproddvdslem  16745  cncongr1  16750  cncongr2  16751  prm2orodd  16774  2mulprm  16776  nnnn0modprm0  16891  prm23lt5  16899  prm23ge5  16900  dvdsprmpweqnn  16970  dvdsprmpweqle  16971  oddprmdvds  16988  prmpwdvds  16989  prmreclem4  17004  ramcl  17114  prmgaplem6  17141  prmgaplem7  17142  prmgaplem8  17143  cshwshashlem1  17180  cshwshashlem2  17181  cshwshashlem3  17182  cshwrepswhash1  17187  setsn0fun  17258  setsstruct2  17259  imasleval  17620  mreiincl  17673  mreexexd  17729  inveq  17856  cicsym  17886  cictr  17887  initoid  18083  termoid  18084  initoeu2lem0  18095  initoeu2lem1  18096  initoeu2lem2  18097  initoeu2  18098  fthestrcsetc  18231  fthsetcestrc  18246  drsdirfi  18386  isnmgm  18727  mgmhmlin  18786  issubmgm2  18790  sgrpass  18812  insubm  18908  mgm2nsgrplem3  19013  dfgrp3lem  19135  cyccom  19305  symg2bas  19494  symgfix2  19517  symgextf1  19522  gsmsymgrfix  19529  pmtrprfv3  19555  psgnunilem4  19598  efgi2  19826  0ringnnzr  20660  rnghmsscmap  20766  rnghmsubcsetclem2  20768  rngcinv  20773  funcrngcsetc  20776  funcrngcsetcALT  20777  rhmsscmap  20795  rhmsubcsetclem2  20797  rhmsubcrngclem2  20803  ringcbasbas  20809  funcringcsetc  20810  rhmsubclem4  20824  unichnlidl  21399  rngqiprngimfo  21478  psgndiflemB  21787  psgndiflemA  21788  elfrlmbasn0  21950  lmictra  22032  mpfrcl  22273  gsummoncoe1  22505  mamufacex  22590  matecl  22619  dmatelnd  22690  dmatscmcl  22697  scmateALT  22706  scmatsgrp1  22716  scmatf1  22725  mavmulsolcl  22745  cramerimplem1  22877  cramerimplem2  22878  pmatcollpw3fi1  22982  mp2pm2mplem4  23003  pm2mpfo  23008  chmaidscmat  23042  fvmptnn04ifb  23045  chfacfscmul0  23052  chfacfpmmul0  23056  cayhamlem1  23060  cayhamlem3  23081  cayleyhamilton1  23086  fiinopn  23095  tgcl  23163  distop  23189  isclo2  23282  iscldtop  23289  ssnei2  23310  opnnei  23314  pnfnei  23414  mnfnei  23415  tgcnp  23447  cnpnei  23458  1stcelcls  23655  txcnpi  23802  cnmptcom  23872  fbfinnfr  24035  isfildlem  24051  snfil  24058  fbunfip  24063  fgcl  24072  elfm2  24142  fmco  24155  fbflim2  24171  cnpflf2  24194  flimfcls  24220  tmdgsum  24289  neibl  24695  tngngpim  24853  fgcfil  25467  caubl  25504  volsuplem  25751  ellimc3  26075  dvnadd  26125  dvnres  26127  cpnord  26131  dvnfre  26148  ply1divex  26331  cxpmul2  26891  fsumdvdsmul  27396  zabsle1  27497  gausslemma2dlem1a  27566  gausslemma2dlem3  27569  lgsquad2lem2  27586  2lgs  27608  2sq2  27634  2sqnn0  27639  2sqnn  27640  2sqreultlem  27648  2sqreunnltlem  27651  qabvexp  27827  ltsval2  27857  nolt02o  27896  sltsun1  28018  cutsun12  28020  madebday  28130  mulsprop  28360  precsexlem8  28444  precsexlem9  28445  noseqind  28522  om2noseqrdg  28534  n0cutlt  28589  peano5uzs  28634  expadds  28665  bdaypw2n0bndlem  28693  bdaypw2n0bnd  28694  axcontlem4  29354  umgredgprv  29494  umgrnloop  29495  upgrpredgv  29526  upgredgpr  29529  edglnl  29530  usgredgprvALT  29582  usgrnloopALT  29590  usgredg2v  29614  fusgrfis  29717  nbuhgr2vtx1edgblem  29738  nb3grprlem1  29767  cusgrsize2inds  29840  cusgrfi  29845  fusgrn0degnn0  29886  uspgrloopvtxel  29903  vtxdginducedm1lem4  29929  uhgr0edg0rgrb  29961  wlkl1loop  30024  wlk1walk  30025  upgriswlk  30027  upgrwlkvtxedg  30031  uspgr2wlkeq  30032  wlkv0  30036  wlksoneq1eq2  30049  wlkon2n0  30051  wlkreslem  30054  wlkres  30055  lfgrwlkprop  30072  pthdivtx  30113  2pthnloop  30117  spthonepeq  30138  uhgrwkspthlem2  30140  uhgrwkspth  30141  usgr2wlkneq  30142  usgr2trlncl  30146  usgr2pthlem  30149  usgr2pth  30150  cyclnspth  30187  lfgrn1cycl  30191  usgr2trlncrct  30192  uspgrn2crct  30194  crctcshwlkn0lem3  30198  crctcshwlkn0lem5  30200  wwlknp  30229  wspthneq1eq2  30246  0enwwlksnge1  30250  wlklnwwlkln1  30254  wlkiswwlks2  30261  wlkiswwlksupgr2  30263  wlklnwwlkln2lem  30268  wwlksnred  30278  wwlksnextbi  30280  wwlksnredwwlkn0  30282  wwlksnextwrd  30283  wwlksnextinj  30285  wwlksnextproplem3  30297  wwlksnextprop  30298  wspthsnwspthsnon  30302  wspthsnonn0vne  30303  2pthon3v  30329  umgr2adedgwlkonALT  30333  umgr2wlk  30335  umgr2wlkon  30336  usgrwwlks2on  30344  umgrwwlks2on  30345  elwspths2on  30348  elwspths2onw  30349  usgr2wspthons3  30353  elwwlks2  30355  rusgrnumwwlk  30364  clwwlkccatlem  30377  clwlkclwwlklem2a4  30385  clwlkclwwlklem2a  30386  clwlkclwwlklem2  30388  clwlkclwwlkf1lem3  30394  erclwwlkeqlen  30407  clwwlknwwlksn  30426  loopclwwlkn1b  30430  clwwlkf1  30437  wwlksext2clwwlk  30445  eleclclwwlknlem2  30449  umgr2cwwk2dif  30452  eleclclwwlkn  30464  hashecclwwlkn1  30465  umgrhashecclwwlk  30466  clwwlknonwwlknonb  30494  clwwlknonex2lem2  30496  clwwlknonex2  30497  1pthon2v  30541  upgr3v3e3cycl  30568  uhgr3cyclexlem  30569  uhgr3cyclex  30570  eupth2lem3lem4  30619  frgr3vlem1  30661  frgr3vlem2  30662  3vfriswmgrlem  30665  3vfriswmgr  30666  3cyclfrgrrn1  30673  n4cyclfrgr  30679  frgrncvvdeqlem3  30689  frgrncvvdeqlem6  30692  frgrncvvdeqlem7  30693  frgrncvvdeqlem8  30694  frgrwopreglem4a  30698  frgrwopreglem3  30702  frgrwopreg1  30706  frgrwopreg2  30707  frgrwopreglem5lem  30708  frgrwopreglem5ALT  30710  frgrwopreg  30711  fusgr2wsp2nb  30722  2wspmdisj  30725  numclwwlk1lem2foa  30742  numclwwlk1lem2f1  30745  numclwwlk1lem2fo  30746  numclwwlk1  30749  wlkl0  30755  numclwwlk2lem1  30764  numclwlk2lem2f  30765  numclwlk2lem2f1o  30767  frgrreg  30782  frgrregord013  30783  frgrregord13  30784  friendshipgt3  30786  friendship  30787  eulplig  30874  ipassi  31230  ubthlem2  31260  isch3  31630  shintcli  31718  shmodsi  31778  spansncvi  32041  hoaddsub  32205  eigorthi  32226  pjss2coi  32553  pjnormssi  32557  pj3cor1i  32598  strb  32647  dmdmd  32689  mdsl0  32699  csmdsymi  32723  chrelat2i  32754  mdsymlem3  32794  mdsymlem6  32797  sumdmdlem2  32808  opreu2reuALT  32860  ssrelf  32997  gsumwun  33427  r1filim  35522  trssfir1om  35531  fineqvinfep  35561  trssfir1omregs  35572  karddom  35597  kardsdom  35598  kardexen  35599  onvf1odlem4  35613  spthcycl  35641  loop1cycl  35649  cvmlift2lem1  35814  satfrel  35879  satfrnmapom  35882  fmlafvel  35897  fmla1  35899  gonarlem  35906  gonar  35907  goalrlem  35908  goalr  35909  satffunlem  35913  satffunlem1lem1  35914  satffunlem2lem1  35916  satffun  35921  satefvfmla1  35937  mrsubvrs  36034  mclsax  36081  3ccased  36231  dfon2lem3  36295  rdgprc  36304  cgrextend  36520  btwndiff  36539  btwnconn1lem12  36610  brsegle  36620  broutsideof2  36634  funray  36652  in-ax8  36776  ss-ax8  36777  elicc3  36868  nn0prpwlem  36873  nn0prpw  36874  fnessref  36908  neibastop2lem  36911  filnetlem4  36932  meran1  36962  waj-ax  36965  arg-ax  36967  axtco1from2  37026  dfttc4  37081  mh-inf3f1  37092  mh-regprimbi  37096  bj-nnclavc  37176  bj-con2com  37193  bj-axdd2  37225  bj-alrimg  37246  bj-exlimg  37268  bj-exalimi  37278  bj-eximcom  37279  bj-ssbid1ALT  37327  bj-sb  37352  bj-snsetex  37639  bj-axseprep  37751  bj-axreprepsep  37752  bj-restpw  37774  bj-finsumval0  37969  mptsnunlem  38024  icoreclin  38043  relowlpssretop  38050  inunissunidif  38061  rdgssun  38064  finorwe  38068  domalom  38090  wl-dral1d  38226  wl-exeq  38229  wl-lem-exsb  38261  wl-eujustlem1  38283  poimirlem29  38340  poimirlem32  38343  fdc  38436  seqpo  38438  incsequz  38439  isismty  38492  ismtybndlem  38497  heibor1lem  38500  ismgmOLD  38541  isexid2  38546  ghomco  38582  pridlc  38762  relcnveq3  39016  elrelscnveq3  39316  cdleme18d  41109  tendovalco  41579  cdlemn11pre  42024  dihord2pre  42039  indstrd  43000  unitscyglem3  43004  eu6w  43448  incssnn0  43482  fphpd  43583  jm2.19lem3  43758  setindtr  43791  islssfg2  43838  mpaaeu  43917  ordnexbtwnsuc  44034  oaabsb  44061  succlg  44095  oacl2g  44097  omabs2  44099  omcl2  44100  omcl3g  44101  pr2cv  44314  refimssco  44373  iunrelexpmin1  44474  iunrelexpmin2  44478  trclimalb2  44492  clsk1indlem3  44809  tfindsd  44974  mnurndlem1  45031  nzss  45067  sb5ALT  45274  truniALT  45290  ee223  45383  3orbi123VD  45598  sbc3orgVD  45599  exbirVD  45601  exbiriVD  45602  sbcim2gVD  45623  trsbcVD  45625  truniALTVD  45626  onfrALTlem3VD  45635  onfrALTlem2VD  45637  csbrngVD  45644  19.41rgVD  45650  ax6e2eqVD  45655  ax6e2ndeqVD  45657  2uasbanhVD  45659  sb5ALTVD  45661  vk15.4jVD  45662  infxrunb3rnmpt  46182  stoweidlem26  46780  et-equeucl  47626  hirstL-ax3  47669  rexsb  47876  rexrsb  47877  euoreqb  47886  2reu8i  47890  afvres  47949  tz6.12-afv  47950  afvco2  47953  afv2orxorb  48005  afv2res  48016  tz6.12-afv2  48017  tz6.12i-afv2  48020  dfatcolem  48032  zm1nn  48079  2ffzoeq  48105  smonoord  48154  iccpartiltu  48211  iccpartlt  48213  iccpartltu  48214  iccpartgtl  48215  iccpartgt  48216  iccpartleu  48217  iccpartgel  48218  icceuelpart  48225  iccpartnel  48227  lswn0  48233  ichnreuop  48261  ichreuopeq  48262  prsprel  48276  sprsymrelfvlem  48279  sprsymrelf1lem  48280  sprsymrelfolem2  48282  prproropf1olem4  48295  paireqne  48300  prprelb  48305  reupr  48311  goldbachth  48339  odz2prm2pw  48355  fmtno4prmfac  48364  fmtno4prmfac193  48365  prmdvdsfmtnof1lem2  48377  2pwp1prmfmtno  48382  lighneallem2  48398  lighneallem4b  48401  lighneallem4  48402  requad2  48428  odd2prm2  48523  mogoldbblem  48525  gbepos  48563  gbowgt5  48567  gbowge7  48568  stgoldbwt  48581  sbgoldbwt  48582  sbgoldbst  48583  sbgoldbaltlem1  48584  sbgoldbalt  48586  sbgoldbo  48592  nnsum3primesle9  48599  nnsum4primesodd  48601  nnsum4primesoddALTV  48602  nnsum4primeseven  48605  nnsum4primesevenALTV  48606  bgoldbtbndlem1  48610  bgoldbtbndlem2  48611  bgoldbtbndlem3  48612  bgoldbtbnd  48614  dfnbgr6  48662  isuspgrimlem  48700  uhgrimisgrgric  48736  clnbgrgrim  48739  usgrgrtrirex  48755  isubgr3stgrlem4  48774  grilcbri2  48816  grlicsym  48818  grlictr  48820  gricgrlic  48823  gpgvtxedg0  48868  gpgvtxedg1  48869  gpgedg2ov  48871  gpgedg2iv  48872  pgnioedg1  48913  pgnioedg2  48914  pgnioedg3  48915  pgnioedg4  48916  pgnioedg5  48917  pgnbgreunbgrlem2lem3  48921  pgnbgreunbgrlem3  48923  pgnbgreunbgrlem5lem1  48925  pgnbgreunbgrlem5lem2  48926  pgnbgreunbgrlem5lem3  48927  pgnbgreunbgrlem6  48929  upgrwlkupwlk  48945  uspgrsprf1  48952  lmod0rng  49034  lidldomn1  49036  rngccatidALTV  49077  rngcinvALTV  49081  rhmsubcALTVlem4  49089  funcringcsetcALTV2lem9  49103  ringccatidALTV  49111  ringcbasbasALTV  49117  ztprmneprm  49167  pgrpgt2nabl  49186  lmodvsmdi  49199  ply1mulgsumlem2  49207  lincsumcl  49251  ellcoellss  49255  linindslinci  49268  islinindfis  49269  lincext3  49276  lindslinindimp2lem4  49281  lindslinindsimp2lem5  49282  lindslinindsimp2  49283  lindsrng01  49288  ldepspr  49293  lincresunit3lem1  49299  elfzolborelfzop1  49339  dignn0ldlem  49422  nn0sumshdiglem1  49441  1arymaptf1  49462  2arymaptf1  49473  rrx2xpref1o  49538  rrx2plord2  49542  rrx2plordisom  49543  line2ylem  49571  line2xlem  49573  line2y  49575  itschlc0xyqsol1  49586  inlinecirc02plem  49606  fullthinc  50268  tfis2d  50498  onsetrec  50526