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 ⊢ (𝜓 → (𝜑 → 𝜒))

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  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  412  impd  415  expcom  418  expdcom  419  simplbi2com  507  imdistanri  579  syldbl2  854  jaod  872  orel1  901  pm2.62  912  pm2.75  946  pm2.64  956  ccased  1052  dedlem0b  1058  3impd  1365  3expd  1370  mp3an1i  1478  minimp  1644  meredith  1664  19.35  1900  speimfw  1986  equtrr  2045  equeucl  2047  ax12ev2  2218  sbiedw  2351  cbv1v  2370  exsb  2393  cbv1  2436  ax12b  2458  axc11n  2460  dvelimdf  2483  equvel  2490  dfsb1  2515  sbied  2537  dfmoeu  2565  mo3  2594  mo4  2596  2mo  2678  2eu6  2686  exists2  2691  pm2.61dne  3046  rexlimdv  3164  r19.21v  3190  r19.12  3314  2gencl  3499  3gencl  3500  vtocl2ga  3545  vtocl2gaf  3546  vtocl3gaf  3547  vtocl3ga  3548  vtocl4ga  3550  rspccv  3581  ceqex  3614  mob  3683  euind  3690  reuind  3719  2reu1  3853  sseq2  3965  nelss  4005  rexdifi  4106  reupick2  4286  disjeq0  4413  uneqdifeq  4449  sspw  4569  ssprsseq  4786  preq12b  4811  prnebg  4817  prel12g  4825  3elpr2eq  4867  iinss2  5018  trintss  5231  dtruALT2  5332  reusv2lem1  5360  alxfr  5369  ralxfrALT  5377  exexneq  5407  copsexgw  5463  copsexgwOLD  5464  copsexg  5465  snopeqop  5480  propeqop  5481  opthhausdorff  5491  opthhausdorff0  5492  pofun  5578  solin  5587  frss  5616  2optocl  5748  3optocl  5749  ssrel  5760  ssrel2  5762  ssrelrel  5773  relop  5827  dfres3  5974  asymref2  6108  xpidtr  6113  trin2  6114  poltletr  6123  imadifssran  6140  xp11  6165  relcnvtrg  6258  reuop  6284  tz7.7  6376  ordtr2  6395  suc11  6459  fundif  6574  fss  6712  f0dom0  6752  fv3  6889  tz6.12i  6897  mpteqb  6999  fveqdmss  7063  eldmrexrnb  7077  funopsnOLD  7135  funsndifnop  7138  tpres  7189  funfvima  7218  fvclss  7229  f1veqaeq  7244  fvf1pr  7295  isoselem  7329  oprabv  7460  ovg  7565  elovmpt3rab1  7660  sorpsscmpl  7721  iunpw  7758  trom  7859  limom  7866  peano5  7878  focdmex  7941  funelss  8032  funeldmdif  8033  bropopvvv  8073  bropfvvvvlem  8074  f1o2ndf1  8105  poxp  8112  soxp  8113  poxp2  8127  frxp2  8128  frxp3  8135  suppimacnv  8158  ressuppss  8167  ressuppssdif  8169  tposfn2  8232  wfr3g  8304  onnseq  8319  smoel  8335  smogt  8342  smoiso2  8344  tfr3  8374  tz7.48-2  8417  tz7.48-3  8419  tz7.49  8420  oecl  8510  oaordex  8531  oalimcl  8533  oaass  8534  omordi  8539  omlimcl  8551  odi  8552  omeulem1  8555  oen0  8560  nnawordi  8595  nnaass  8596  nnmordi  8605  omabs  8625  omsmolem  8631  naddssim  8660  brinxper  8712  iiner  8775  2ecoptocl  8794  3ecoptocl  8795  undifixp  8920  xpdom2  9048  xpf1o  9115  infensuc  9131  findcard2  9137  php  9179  isinf  9213  unblem2  9241  fodomfir  9275  infssuni  9291  finsschain  9304  fsuppunfi  9336  fsuppunbi  9337  marypha1  9382  hartogs  9494  card2on  9504  card2inf  9505  xpwdomg  9535  elirrvOLD  9548  elirrvOLDOLD  9549  en3lp  9571  preleqg  9572  inf3lem1  9585  inf3lem2  9586  inf3lem3  9587  inf3lem5  9589  noinfep  9617  ttrclss  9677  ttrclselem2  9683  trcl  9685  tcel  9700  frr3g  9716  rankonidlem  9788  scottex  9847  djuunxp  9895  eldju2ndl  9898  updjud  9908  dif1card  9982  fodomnum  10029  cardaleph  10061  kmlem9  10130  kmlem13  10134  cflim2  10235  cfsmolem  10242  infpssrlem3  10277  isfin7-2  10368  fin1a2lem6  10377  fin1a2lem12  10383  domtriomlem  10414  axdc3lem4  10425  axdc4lem  10427  zorn2lem3  10470  zorn2lem4  10471  zorn2lem5  10472  zorn2lem7  10474  zornn0g  10477  axdclem2  10492  ondomon  10535  alephval2  10545  cfpwsdom  10557  wuncval2  10720  grupr  10770  gruiun  10772  ingru  10788  grothomex  10802  indpi  10880  nqereu  10902  prlem934  11006  reclem2pr  11021  mulgt0sr  11078  supsrlem  11084  1re  11196  dedekind  11361  lemul1a  12060  squeeze0  12109  peano5nni  12227  nnadddir  12283  nnunb  12491  nn0lt2  12650  nn0le2is012  12651  fzind  12685  nn0ind-raph  12687  zindd  12688  uzin  12889  nn01to3  12956  xnn0xadd0  13264  xmulasslem  13302  icoshft  13491  fzen  13560  uzsubsubfz  13565  elfz0ubfz0  13651  elfz0fzfz0  13652  fz0fzelfz0  13653  elfzmlbp  13658  elfzodifsumelfzo  13751  ssfzo12bi  13781  fzoopth  13782  elfzonelfzo  13789  elfznelfzo  13793  injresinjlem  13810  injresinj  13811  modfzo0difsn  13970  modsumfzodifsn  13971  addmodlteq  13973  ssnn0fi  14012  fsuppmapnn0fiub0  14020  expcllem  14099  expeq0  14119  mulexp  14128  leexp2r  14201  bernneq  14256  facdiv  14314  hasheqf1oi  14378  hashnn0n0nn  14418  hashss  14436  hashgt12el  14449  hashgt12el2  14450  hashimarni  14468  hashle2pr  14504  pr2pwpr  14506  hashge2el2dif  14507  hashge2el2difr  14508  hashtpg  14512  hashge3el3dif  14514  exprelprel  14517  hash1to3  14519  hash3tpde  14520  tpfo  14527  fundmge2nop0  14529  fi1uzind  14534  ccatsymb  14610  swrdnd  14682  swrdnd2  14683  swrdnnn0nd  14684  swrdnd0  14685  pfxnd0  14716  swrdswrdlem  14731  swrdswrd  14732  pfxccatin12lem2a  14754  pfxccatin12lem1  14755  swrdccatin2  14756  pfxccatin12lem2  14758  pfxccatin12lem3  14759  pfxccat3  14761  swrdccat  14762  swrdccat3blem  14766  repsdf2  14805  repswswrd  14811  cshwidxmod  14830  cshwidx0  14833  cshf1  14837  cshweqrep  14848  cshw1  14849  2cshwcshw  14852  scshwfzeqfzo  14853  cshwcsh2id  14855  wwlktovfo  14985  relexpaddg  15080  iseraltlem2  15724  modfsummods  15835  clim2prod  15932  prodfn0  15938  prodfrec  15939  prodmo  15980  fprodabs  16018  binomfallfac  16085  fprodefsum  16139  dvdsaddre2b  16355  addmodlteqALT  16373  oddge22np1  16397  nn0enne  16425  nn0o1gt2  16429  sumeven  16435  sumodd  16436  dvdslegcd  16552  gcdneg  16570  dfgcd2  16594  rplpwr  16606  lcmf  16681  lcmftp  16684  lcmfunsnlem2lem1  16686  lcmfunsnlem2  16688  lcmfdvdsb  16691  coprmdvds1  16700  qredeq  16705  coprmprod  16709  coprmproddvdslem  16710  cncongr1  16715  cncongr2  16716  prm2orodd  16739  2mulprm  16741  nnnn0modprm0  16856  prm23lt5  16864  prm23ge5  16865  dvdsprmpweqnn  16935  dvdsprmpweqle  16936  oddprmdvds  16953  prmpwdvds  16954  prmreclem4  16969  ramcl  17079  prmgaplem6  17106  prmgaplem7  17107  prmgaplem8  17108  cshwshashlem1  17145  cshwshashlem2  17146  cshwshashlem3  17147  cshwrepswhash1  17152  setsn0fun  17223  setsstruct2  17224  imasleval  17585  mreiincl  17638  mreexexd  17694  inveq  17821  cicsym  17851  cictr  17852  initoid  18048  termoid  18049  initoeu2lem0  18060  initoeu2lem1  18061  initoeu2lem2  18062  initoeu2  18063  fthestrcsetc  18196  fthsetcestrc  18211  drsdirfi  18351  isnmgm  18692  mgmhmlin  18747  issubmgm2  18751  sgrpass  18773  insubm  18867  mgm2nsgrplem3  18972  dfgrp3lem  19095  cyccom  19265  symg2bas  19454  symgfix2  19477  symgextf1  19482  gsmsymgrfix  19489  pmtrprfv3  19515  psgnunilem4  19558  efgi2  19786  0ringnnzr  20600  rnghmsscmap  20706  rnghmsubcsetclem2  20708  rngcinv  20713  funcrngcsetc  20716  funcrngcsetcALT  20717  rhmsscmap  20735  rhmsubcsetclem2  20737  rhmsubcrngclem2  20743  ringcbasbas  20749  funcringcsetc  20750  rhmsubclem4  20764  unichnlidl  21331  rngqiprngimfo  21403  psgndiflemB  21710  psgndiflemA  21711  elfrlmbasn0  21873  lmictra  21955  mpfrcl  22196  gsummoncoe1  22429  mamufacex  22514  matecl  22543  dmatelnd  22614  dmatscmcl  22621  scmateALT  22630  scmatsgrp1  22640  scmatf1  22649  mavmulsolcl  22669  cramerimplem1  22801  cramerimplem2  22802  pmatcollpw3fi1  22906  mp2pm2mplem4  22927  pm2mpfo  22932  chmaidscmat  22966  fvmptnn04ifb  22969  chfacfscmul0  22976  chfacfpmmul0  22980  cayhamlem1  22984  cayhamlem3  23005  cayleyhamilton1  23010  fiinopn  23019  tgcl  23087  distop  23113  isclo2  23206  iscldtop  23213  ssnei2  23234  opnnei  23238  pnfnei  23338  mnfnei  23339  tgcnp  23371  cnpnei  23382  1stcelcls  23579  txcnpi  23726  cnmptcom  23796  fbfinnfr  23959  isfildlem  23975  snfil  23982  fbunfip  23987  fgcl  23996  elfm2  24066  fmco  24079  fbflim2  24095  cnpflf2  24118  flimfcls  24144  tmdgsum  24213  neibl  24619  tngngpim  24777  fgcfil  25391  caubl  25428  volsuplem  25675  ellimc3  25999  dvnadd  26049  dvnres  26051  cpnord  26055  dvnfre  26072  ply1divex  26255  cxpmul2  26812  fsumdvdsmul  27317  zabsle1  27418  gausslemma2dlem1a  27487  gausslemma2dlem3  27490  lgsquad2lem2  27507  2lgs  27529  2sq2  27555  2sqnn0  27560  2sqnn  27561  2sqreultlem  27569  2sqreunnltlem  27572  qabvexp  27748  ltsval2  27778  nolt02o  27817  sltsun1  27939  cutsun12  27941  madebday  28051  mulsprop  28281  precsexlem8  28365  precsexlem9  28366  noseqind  28443  om2noseqrdg  28455  n0cutlt  28510  peano5uzs  28555  expadds  28586  bdaypw2n0bndlem  28614  bdaypw2n0bnd  28615  axcontlem4  29226  umgredgprv  29366  umgrnloop  29367  upgrpredgv  29398  upgredgpr  29401  edglnl  29402  usgredgprvALT  29454  usgrnloopALT  29462  usgredg2v  29486  fusgrfis  29589  nbuhgr2vtx1edgblem  29610  nb3grprlem1  29639  cusgrsize2inds  29712  cusgrfi  29717  fusgrn0degnn0  29758  uspgrloopvtxel  29775  vtxdginducedm1lem4  29801  uhgr0edg0rgrb  29833  wlkl1loop  29896  wlk1walk  29897  upgriswlk  29899  upgrwlkvtxedg  29903  uspgr2wlkeq  29904  wlkv0  29908  wlksoneq1eq2  29921  wlkon2n0  29923  wlkreslem  29926  wlkres  29927  lfgrwlkprop  29944  pthdivtx  29985  2pthnloop  29989  spthonepeq  30010  uhgrwkspthlem2  30012  uhgrwkspth  30013  usgr2wlkneq  30014  usgr2trlncl  30018  usgr2pthlem  30021  usgr2pth  30022  cyclnspth  30059  lfgrn1cycl  30063  usgr2trlncrct  30064  uspgrn2crct  30066  crctcshwlkn0lem3  30070  crctcshwlkn0lem5  30072  wwlknp  30101  wspthneq1eq2  30118  0enwwlksnge1  30122  wlklnwwlkln1  30126  wlkiswwlks2  30133  wlkiswwlksupgr2  30135  wlklnwwlkln2lem  30140  wwlksnred  30150  wwlksnextbi  30152  wwlksnredwwlkn0  30154  wwlksnextwrd  30155  wwlksnextinj  30157  wwlksnextproplem3  30169  wwlksnextprop  30170  wspthsnwspthsnon  30174  wspthsnonn0vne  30175  2pthon3v  30201  umgr2adedgwlkonALT  30205  umgr2wlk  30207  umgr2wlkon  30208  usgrwwlks2on  30216  umgrwwlks2on  30217  elwspths2on  30220  elwspths2onw  30221  usgr2wspthons3  30225  elwwlks2  30227  rusgrnumwwlk  30236  clwwlkccatlem  30249  clwlkclwwlklem2a4  30257  clwlkclwwlklem2a  30258  clwlkclwwlklem2  30260  clwlkclwwlkf1lem3  30266  erclwwlkeqlen  30279  clwwlknwwlksn  30298  loopclwwlkn1b  30302  clwwlkf1  30309  wwlksext2clwwlk  30317  eleclclwwlknlem2  30321  umgr2cwwk2dif  30324  eleclclwwlkn  30336  hashecclwwlkn1  30337  umgrhashecclwwlk  30338  clwwlknonwwlknonb  30366  clwwlknonex2lem2  30368  clwwlknonex2  30369  1pthon2v  30413  upgr3v3e3cycl  30440  uhgr3cyclexlem  30441  uhgr3cyclex  30442  eupth2lem3lem4  30491  frgr3vlem1  30533  frgr3vlem2  30534  3vfriswmgrlem  30537  3vfriswmgr  30538  3cyclfrgrrn1  30545  n4cyclfrgr  30551  frgrncvvdeqlem3  30561  frgrncvvdeqlem6  30564  frgrncvvdeqlem7  30565  frgrncvvdeqlem8  30566  frgrwopreglem4a  30570  frgrwopreglem3  30574  frgrwopreg1  30578  frgrwopreg2  30579  frgrwopreglem5lem  30580  frgrwopreglem5ALT  30582  frgrwopreg  30583  fusgr2wsp2nb  30594  2wspmdisj  30597  numclwwlk1lem2foa  30614  numclwwlk1lem2f1  30617  numclwwlk1lem2fo  30618  numclwwlk1  30621  wlkl0  30627  numclwwlk2lem1  30636  numclwlk2lem2f  30637  numclwlk2lem2f1o  30639  frgrreg  30654  frgrregord013  30655  frgrregord13  30656  friendshipgt3  30658  friendship  30659  eulplig  30746  ipassi  31102  ubthlem2  31132  isch3  31502  shintcli  31590  shmodsi  31650  spansncvi  31913  hoaddsub  32077  eigorthi  32098  pjss2coi  32425  pjnormssi  32429  pj3cor1i  32470  strb  32519  dmdmd  32561  mdsl0  32571  csmdsymi  32595  chrelat2i  32626  mdsymlem3  32666  mdsymlem6  32669  sumdmdlem2  32680  opreu2reuALT  32733  ssrelf  32872  gsumwun  33309  r1filim  35412  trssfir1om  35419  fineqvinfep  35433  trssfir1omregs  35444  onvf1odlem4  35461  spthcycl  35492  loop1cycl  35500  cvmlift2lem1  35665  satfrel  35730  satfrnmapom  35733  fmlafvel  35748  fmla1  35750  gonarlem  35757  gonar  35758  goalrlem  35759  goalr  35760  satffunlem  35764  satffunlem1lem1  35765  satffunlem2lem1  35767  satffun  35772  satefvfmla1  35788  mrsubvrs  35885  mclsax  35932  3ccased  36082  dfon2lem3  36146  rdgprc  36155  cgrextend  36371  btwndiff  36390  btwnconn1lem12  36461  brsegle  36471  broutsideof2  36485  funray  36503  in-ax8  36597  ss-ax8  36598  elicc3  36690  nn0prpwlem  36695  nn0prpw  36696  fnessref  36730  neibastop2lem  36733  filnetlem4  36754  meran1  36784  waj-ax  36787  arg-ax  36789  axtco1from2  36848  dfttc4  36903  mh-inf3f1  36914  mh-regprimbi  36918  bj-nnclavc  36998  bj-con2com  37015  bj-axdd2  37047  bj-alrimg  37068  bj-exlimg  37090  bj-exalimi  37100  bj-eximcom  37101  bj-ssbid1ALT  37149  bj-sb  37174  bj-snsetex  37460  bj-axseprep  37571  bj-axreprepsep  37572  bj-restpw  37594  bj-finsumval0  37789  mptsnunlem  37844  icoreclin  37863  relowlpssretop  37870  inunissunidif  37881  rdgssun  37884  finorwe  37888  domalom  37910  wl-dral1d  38046  wl-exeq  38049  wl-lem-exsb  38081  wl-eujustlem1  38103  poimirlem29  38160  poimirlem32  38163  fdc  38256  seqpo  38258  incsequz  38259  isismty  38312  ismtybndlem  38317  heibor1lem  38320  ismgmOLD  38361  isexid2  38366  ghomco  38402  pridlc  38582  relcnveq3  38838  elrelscnveq3  39138  cdleme18d  40931  tendovalco  41401  cdlemn11pre  41846  dihord2pre  41861  indstrd  42822  unitscyglem3  42826  eu6w  43270  incssnn0  43304  fphpd  43405  jm2.19lem3  43580  setindtr  43613  islssfg2  43660  mpaaeu  43739  ordnexbtwnsuc  43856  oaabsb  43883  succlg  43917  oacl2g  43919  omabs2  43921  omcl2  43922  omcl3g  43923  pr2cv  44136  refimssco  44195  iunrelexpmin1  44296  iunrelexpmin2  44300  trclimalb2  44314  clsk1indlem3  44631  tfindsd  44798  mnurndlem1  44855  nzss  44891  sb5ALT  45099  truniALT  45115  ee223  45208  3orbi123VD  45423  sbc3orgVD  45424  exbirVD  45426  exbiriVD  45427  sbcim2gVD  45448  trsbcVD  45450  truniALTVD  45451  onfrALTlem3VD  45460  onfrALTlem2VD  45462  csbrngVD  45469  19.41rgVD  45475  ax6e2eqVD  45480  ax6e2ndeqVD  45482  2uasbanhVD  45484  sb5ALTVD  45486  vk15.4jVD  45487  infxrunb3rnmpt  46000  stoweidlem26  46598  et-equeucl  47444  hirstL-ax3  47484  rexsb  47691  rexrsb  47692  euoreqb  47701  2reu8i  47705  afvres  47764  tz6.12-afv  47765  afvco2  47768  afv2orxorb  47820  afv2res  47831  tz6.12-afv2  47832  tz6.12i-afv2  47835  dfatcolem  47847  zm1nn  47894  2ffzoeq  47920  smonoord  47969  iccpartiltu  48026  iccpartlt  48028  iccpartltu  48029  iccpartgtl  48030  iccpartgt  48031  iccpartleu  48032  iccpartgel  48033  icceuelpart  48040  iccpartnel  48042  lswn0  48048  ichnreuop  48076  ichreuopeq  48077  prsprel  48091  sprsymrelfvlem  48094  sprsymrelf1lem  48095  sprsymrelfolem2  48097  prproropf1olem4  48110  paireqne  48115  prprelb  48120  reupr  48126  goldbachth  48154  odz2prm2pw  48170  fmtno4prmfac  48179  fmtno4prmfac193  48180  prmdvdsfmtnof1lem2  48192  2pwp1prmfmtno  48197  lighneallem2  48213  lighneallem4b  48216  lighneallem4  48217  requad2  48243  odd2prm2  48338  mogoldbblem  48340  gbepos  48378  gbowgt5  48382  gbowge7  48383  stgoldbwt  48396  sbgoldbwt  48397  sbgoldbst  48398  sbgoldbaltlem1  48399  sbgoldbalt  48401  sbgoldbo  48407  nnsum3primesle9  48414  nnsum4primesodd  48416  nnsum4primesoddALTV  48417  nnsum4primeseven  48420  nnsum4primesevenALTV  48421  bgoldbtbndlem1  48425  bgoldbtbndlem2  48426  bgoldbtbndlem3  48427  bgoldbtbnd  48429  dfnbgr6  48477  isuspgrimlem  48515  uhgrimisgrgric  48551  clnbgrgrim  48554  usgrgrtrirex  48570  isubgr3stgrlem4  48589  grilcbri2  48631  grlicsym  48633  grlictr  48635  gricgrlic  48638  gpgvtxedg0  48683  gpgvtxedg1  48684  gpgedg2ov  48686  gpgedg2iv  48687  pgnioedg1  48728  pgnioedg2  48729  pgnioedg3  48730  pgnioedg4  48731  pgnioedg5  48732  pgnbgreunbgrlem2lem3  48736  pgnbgreunbgrlem3  48738  pgnbgreunbgrlem5lem1  48740  pgnbgreunbgrlem5lem2  48741  pgnbgreunbgrlem5lem3  48742  pgnbgreunbgrlem6  48744  upgrwlkupwlk  48760  uspgrsprf1  48767  lmod0rng  48849  lidldomn1  48851  rngccatidALTV  48892  rngcinvALTV  48896  rhmsubcALTVlem4  48904  funcringcsetcALTV2lem9  48918  ringccatidALTV  48926  ringcbasbasALTV  48932  ztprmneprm  48978  pgrpgt2nabl  48997  lmodvsmdi  49010  ply1mulgsumlem2  49018  lincsumcl  49062  ellcoellss  49066  linindslinci  49079  islinindfis  49080  lincext3  49087  lindslinindimp2lem4  49092  lindslinindsimp2lem5  49093  lindslinindsimp2  49094  lindsrng01  49099  ldepspr  49104  lincresunit3lem1  49110  elfzolborelfzop1  49150  dignn0ldlem  49233  nn0sumshdiglem1  49252  1arymaptf1  49273  2arymaptf1  49284  rrx2xpref1o  49349  rrx2plord2  49353  rrx2plordisom  49354  line2ylem  49382  line2xlem  49384  line2y  49386  itschlc0xyqsol1  49397  inlinecirc02plem  49417  fullthinc  50079  tfis2d  50309  onsetrec  50337