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  841  jaod  859  orel1  888  pm2.62  899  pm2.75  933  pm2.64  943  ccased  1038  dedlem0b  1044  3impd  1349  3expd  1354  mp3an1i  1456  minimp  1621  meredith  1641  19.35  1877  speimfw  1963  equtrr  2022  equeucl  2024  ax12ev2  2181  sbiedw  2315  cbv1v  2334  exsb  2357  cbv1  2400  ax12b  2422  axc11n  2424  dvelimdf  2447  equvel  2454  dfsb1  2479  sbied  2501  dfmoeu  2529  mo3  2557  mo4  2559  2mo  2641  2eu6  2650  exists2  2655  pm2.61dne  3011  rexlimdv  3128  r19.21v  3154  r19.12  3279  2gencl  3481  3gencl  3482  vtocl2ga  3535  vtocl2gaf  3536  vtocl3gaf  3538  vtocl3ga  3540  vtocl4ga  3543  rspccv  3576  ceqex  3609  mob  3679  euind  3686  reuind  3715  2reu1  3851  sseq2  3964  nelss  4003  rexdifi  4103  reupick2  4284  disjeq0  4409  uneqdifeq  4446  sspw  4564  ssprsseq  4779  preq12b  4804  prnebg  4810  prel12g  4818  3elpr2eq  4860  iinss2  5009  trintss  5220  dtruALT2  5312  reusv2lem1  5340  alxfr  5349  ralxfrALT  5357  exexneq  5381  dtruOLD  5388  copsexgw  5437  copsexg  5438  snopeqop  5453  propeqop  5454  opthhausdorff  5464  opthhausdorff0  5465  pofun  5549  solin  5558  frss  5587  2optocl  5719  3optocl  5720  ssrel  5730  ssrel2  5732  ssrelrel  5743  relop  5797  dfres3  5939  asymref2  6070  xpidtr  6075  trin2  6076  poltletr  6085  imadifssran  6104  xp11  6128  relcnvtrg  6219  reuop  6245  tz7.7  6337  ordtr2  6356  suc11  6420  fundif  6535  fss  6672  f0dom0  6712  fv3  6844  tz6.12i  6852  mpteqb  6953  fveqdmss  7016  eldmrexrnb  7030  funopsn  7086  funsndifnop  7089  tpres  7141  funfvima  7170  fvclss  7181  f1veqaeq  7197  fvf1pr  7248  isoselem  7282  oprabv  7413  ovg  7518  elovmpt3rab1  7613  sorpsscmpl  7674  iunpw  7711  trom  7815  limom  7822  peano5  7833  focdmex  7898  funelss  7989  funeldmdif  7990  bropopvvv  8030  bropfvvvvlem  8031  f1o2ndf1  8062  poxp  8068  soxp  8069  poxp2  8083  frxp2  8084  frxp3  8091  suppimacnv  8114  ressuppss  8123  ressuppssdif  8125  tposfn2  8188  wfr3g  8259  onnseq  8274  smoel  8290  smogt  8297  smoiso2  8299  tfr3  8328  tz7.48-2  8371  tz7.48-3  8373  tz7.49  8374  oecl  8462  oaordex  8483  oalimcl  8485  oaass  8486  omordi  8491  omlimcl  8503  odi  8504  omeulem1  8507  oen0  8511  nnawordi  8546  nnaass  8547  nnmordi  8556  omabs  8576  omsmolem  8582  naddssim  8610  brinxper  8661  iiner  8723  2ecoptocl  8742  3ecoptocl  8743  undifixp  8868  xpdom2  8996  xpf1o  9063  infensuc  9079  findcard2  9088  php  9131  isinf  9165  isinfOLD  9166  unblem2  9198  fodomfir  9237  infssuni  9255  finsschain  9268  fsuppunfi  9297  fsuppunbi  9298  marypha1  9343  hartogs  9455  card2on  9465  card2inf  9466  xpwdomg  9496  elirrv  9508  elirrvOLD  9509  en3lp  9529  preleqg  9530  inf3lem1  9543  inf3lem2  9544  inf3lem3  9545  inf3lem5  9547  noinfep  9575  ttrclss  9635  ttrclselem2  9641  trcl  9643  tcel  9660  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  10485  cfpwsdom  10497  wuncval2  10660  grupr  10710  gruiun  10712  ingru  10728  grothomex  10742  indpi  10820  nqereu  10842  prlem934  10946  reclem2pr  10961  mulgt0sr  11018  supsrlem  11024  1re  11134  dedekind  11297  lemul1a  11996  squeeze0  12046  peano5nni  12149  nnunb  12398  nn0lt2  12557  nn0le2is012  12558  fzind  12592  nn0ind-raph  12594  zindd  12595  eluzaddOLD  12788  uzin  12793  nn01to3  12860  xnn0xadd0  13167  xmulasslem  13205  icoshft  13394  fzen  13462  uzsubsubfz  13467  elfz0ubfz0  13553  elfz0fzfz0  13554  fz0fzelfz0  13555  elfzmlbp  13560  elfzodifsumelfzo  13652  ssfzo12bi  13682  fzoopth  13683  elfzonelfzo  13690  elfznelfzo  13693  injresinjlem  13708  injresinj  13709  modfzo0difsn  13868  modsumfzodifsn  13869  addmodlteq  13871  ssnn0fi  13910  fsuppmapnn0fiub0  13918  expcllem  13997  expeq0  14017  mulexp  14026  leexp2r  14099  bernneq  14154  facdiv  14212  hasheqf1oi  14276  hashnn0n0nn  14316  hashss  14334  hashgt12el  14347  hashgt12el2  14348  hashimarni  14366  hashle2pr  14402  pr2pwpr  14404  hashge2el2dif  14405  hashge2el2difr  14406  hashtpg  14410  hashge3el3dif  14412  exprelprel  14415  hash1to3  14417  hash3tpde  14418  tpfo  14425  fundmge2nop0  14427  fi1uzind  14432  ccatsymb  14507  swrdnd  14579  swrdnd2  14580  swrdnnn0nd  14581  swrdnd0  14582  pfxnd0  14613  swrdswrdlem  14628  swrdswrd  14629  pfxccatin12lem2a  14651  pfxccatin12lem1  14652  swrdccatin2  14653  pfxccatin12lem2  14655  pfxccatin12lem3  14656  pfxccat3  14658  swrdccat  14659  swrdccat3blem  14663  repsdf2  14702  repswswrd  14708  cshwidxmod  14727  cshwidx0  14730  cshf1  14734  cshweqrep  14745  cshw1  14746  cshwsexaOLD  14749  2cshwcshw  14750  scshwfzeqfzo  14751  cshwcsh2id  14753  wwlktovfo  14883  relexpaddg  14978  iseraltlem2  15608  modfsummods  15718  clim2prod  15813  prodfn0  15819  prodfrec  15820  prodmo  15861  fprodabs  15899  binomfallfac  15966  fprodefsum  16020  dvdsaddre2b  16236  addmodlteqALT  16254  oddge22np1  16278  nn0enne  16306  nn0o1gt2  16310  sumeven  16316  sumodd  16317  dvdslegcd  16433  gcdneg  16451  dfgcd2  16475  rplpwr  16487  lcmf  16562  lcmftp  16565  lcmfunsnlem2lem1  16567  lcmfunsnlem2  16569  lcmfdvdsb  16572  coprmdvds1  16581  qredeq  16586  coprmprod  16590  coprmproddvdslem  16591  cncongr1  16596  cncongr2  16597  prm2orodd  16620  2mulprm  16622  nnnn0modprm0  16736  prm23lt5  16744  prm23ge5  16745  dvdsprmpweqnn  16815  dvdsprmpweqle  16816  oddprmdvds  16833  prmpwdvds  16834  prmreclem4  16849  ramcl  16959  prmgaplem6  16986  prmgaplem7  16987  prmgaplem8  16988  cshwshashlem1  17025  cshwshashlem2  17026  cshwshashlem3  17027  cshwrepswhash1  17032  setsn0fun  17102  setsstruct2  17103  imasleval  17463  mreiincl  17516  mreexexd  17572  inveq  17699  cicsym  17729  cictr  17730  initoid  17926  termoid  17927  initoeu2lem0  17938  initoeu2lem1  17939  initoeu2lem2  17940  initoeu2  17941  fthestrcsetc  18074  fthsetcestrc  18089  drsdirfi  18229  isnmgm  18536  mgmhmlin  18591  issubmgm2  18595  sgrpass  18617  insubm  18710  mgm2nsgrplem3  18812  dfgrp3lem  18935  cyccom  19100  symg2bas  19290  symgfix2  19313  symgextf1  19318  gsmsymgrfix  19325  pmtrprfv3  19351  psgnunilem4  19394  efgi2  19622  0ringnnzr  20428  rnghmsscmap  20533  rnghmsubcsetclem2  20535  rngcinv  20540  funcrngcsetc  20543  funcrngcsetcALT  20544  rhmsscmap  20562  rhmsubcsetclem2  20564  rhmsubcrngclem2  20570  ringcbasbas  20576  funcringcsetc  20577  rhmsubclem4  20591  rngqiprngimfo  21226  psgndiflemB  21525  psgndiflemA  21526  elfrlmbasn0  21688  lmictra  21770  mpfrcl  22008  gsummoncoe1  22211  mamufacex  22299  matecl  22328  dmatelnd  22399  dmatscmcl  22406  scmateALT  22415  scmatsgrp1  22425  scmatf1  22434  mavmulsolcl  22454  cramerimplem1  22586  cramerimplem2  22587  pmatcollpw3fi1  22691  mp2pm2mplem4  22712  pm2mpfo  22717  chmaidscmat  22751  fvmptnn04ifb  22754  chfacfscmul0  22761  chfacfpmmul0  22765  cayhamlem1  22769  cayhamlem3  22790  cayleyhamilton1  22795  fiinopn  22804  tgcl  22872  distop  22898  isclo2  22991  iscldtop  22998  ssnei2  23019  opnnei  23023  pnfnei  23123  mnfnei  23124  tgcnp  23156  cnpnei  23167  1stcelcls  23364  txcnpi  23511  cnmptcom  23581  fbfinnfr  23744  isfildlem  23760  snfil  23767  fbunfip  23772  fgcl  23781  elfm2  23851  fmco  23864  fbflim2  23880  cnpflf2  23903  flimfcls  23929  tmdgsum  23998  neibl  24405  tngngpim  24563  fgcfil  25187  caubl  25224  volsuplem  25472  ellimc3  25796  dvnadd  25847  dvnres  25849  cpnord  25853  dvnfre  25872  ply1divex  26058  cxpmul2  26614  fsumdvdsmul  27121  zabsle1  27223  gausslemma2dlem1a  27292  gausslemma2dlem3  27295  lgsquad2lem2  27312  2lgs  27334  2sq2  27360  2sqnn0  27365  2sqnn  27366  2sqreultlem  27374  2sqreunnltlem  27377  qabvexp  27553  sltval2  27584  nolt02o  27623  ssltun1  27737  scutun12  27739  madebday  27832  mulsprop  28056  precsexlem8  28139  precsexlem9  28140  noseqind  28209  om2noseqrdg  28221  n0cutlt  28272  peano5uzs  28315  expadds  28345  axcontlem4  28930  umgredgprv  29070  umgrnloop  29071  upgrpredgv  29102  upgredgpr  29105  edglnl  29106  usgredgprvALT  29158  usgrnloopALT  29166  usgredg2v  29190  fusgrfis  29293  nbuhgr2vtx1edgblem  29314  nb3grprlem1  29343  cusgrsize2inds  29417  cusgrfi  29422  fusgrn0degnn0  29463  uspgrloopvtxel  29480  vtxdginducedm1lem4  29506  uhgr0edg0rgrb  29538  wlkl1loop  29601  wlk1walk  29602  upgriswlk  29604  upgrwlkvtxedg  29608  uspgr2wlkeq  29609  wlkv0  29613  wlksoneq1eq2  29626  wlkon2n0  29628  wlkreslem  29631  wlkres  29632  lfgrwlkprop  29649  pthdivtx  29690  2pthnloop  29694  spthonepeq  29715  uhgrwkspthlem2  29717  uhgrwkspth  29718  usgr2wlkneq  29719  usgr2trlncl  29723  usgr2pthlem  29726  usgr2pth  29727  cyclnspth  29764  lfgrn1cycl  29768  usgr2trlncrct  29769  uspgrn2crct  29771  crctcshwlkn0lem3  29775  crctcshwlkn0lem5  29777  wwlknp  29806  wspthneq1eq2  29823  0enwwlksnge1  29827  wlklnwwlkln1  29831  wlkiswwlks2  29838  wlkiswwlksupgr2  29840  wlklnwwlkln2lem  29845  wwlksnred  29855  wwlksnextbi  29857  wwlksnredwwlkn0  29859  wwlksnextwrd  29860  wwlksnextinj  29862  wwlksnextproplem3  29874  wwlksnextprop  29875  wspthsnwspthsnon  29879  wspthsnonn0vne  29880  2pthon3v  29906  umgr2adedgwlkonALT  29910  umgr2wlk  29912  umgr2wlkon  29913  umgrwwlks2on  29920  elwspths2on  29923  usgr2wspthons3  29927  elwwlks2  29929  rusgrnumwwlk  29938  clwwlkccatlem  29951  clwlkclwwlklem2a4  29959  clwlkclwwlklem2a  29960  clwlkclwwlklem2  29962  clwlkclwwlkf1lem3  29968  erclwwlkeqlen  29981  clwwlknwwlksn  30000  loopclwwlkn1b  30004  clwwlkf1  30011  wwlksext2clwwlk  30019  eleclclwwlknlem2  30023  umgr2cwwk2dif  30026  eleclclwwlkn  30038  hashecclwwlkn1  30039  umgrhashecclwwlk  30040  clwwlknonwwlknonb  30068  clwwlknonex2lem2  30070  clwwlknonex2  30071  1pthon2v  30115  upgr3v3e3cycl  30142  uhgr3cyclexlem  30143  uhgr3cyclex  30144  eupth2lem3lem4  30193  frgr3vlem1  30235  frgr3vlem2  30236  3vfriswmgrlem  30239  3vfriswmgr  30240  3cyclfrgrrn1  30247  n4cyclfrgr  30253  frgrncvvdeqlem3  30263  frgrncvvdeqlem6  30266  frgrncvvdeqlem7  30267  frgrncvvdeqlem8  30268  frgrwopreglem4a  30272  frgrwopreglem3  30276  frgrwopreg1  30280  frgrwopreg2  30281  frgrwopreglem5lem  30282  frgrwopreglem5ALT  30284  frgrwopreg  30285  fusgr2wsp2nb  30296  2wspmdisj  30299  numclwwlk1lem2foa  30316  numclwwlk1lem2f1  30319  numclwwlk1lem2fo  30320  numclwwlk1  30323  wlkl0  30329  numclwwlk2lem1  30338  numclwlk2lem2f  30339  numclwlk2lem2f1o  30341  frgrreg  30356  frgrregord013  30357  frgrregord13  30358  friendshipgt3  30360  friendship  30361  eulplig  30447  ipassi  30803  ubthlem2  30833  isch3  31203  shintcli  31291  shmodsi  31351  spansncvi  31614  hoaddsub  31778  eigorthi  31799  pjss2coi  32126  pjnormssi  32130  pj3cor1i  32171  strb  32220  dmdmd  32262  mdsl0  32272  csmdsymi  32296  chrelat2i  32327  mdsymlem3  32367  mdsymlem6  32370  sumdmdlem2  32381  opreu2reuALT  32439  ssrelf  32576  gsumwun  33031  onvf1odlem4  35078  spthcycl  35101  loop1cycl  35109  cvmlift2lem1  35274  satfrel  35339  satfrnmapom  35342  fmlafvel  35357  fmla1  35359  gonarlem  35366  gonar  35367  goalrlem  35368  goalr  35369  satffunlem  35373  satffunlem1lem1  35374  satffunlem2lem1  35376  satffun  35381  satefvfmla1  35397  mrsubvrs  35494  mclsax  35541  3ccased  35691  dfon2lem3  35758  rdgprc  35767  cgrextend  35981  btwndiff  36000  btwnconn1lem12  36071  brsegle  36081  broutsideof2  36095  funray  36113  in-ax8  36197  ss-ax8  36198  elicc3  36290  nn0prpwlem  36295  nn0prpw  36296  fnessref  36330  neibastop2lem  36333  filnetlem4  36354  meran1  36384  waj-ax  36387  arg-ax  36389  bj-nnclavc  36521  bj-con2com  36534  bj-axdd2  36565  bj-alrimg  36592  bj-exlimg  36596  bj-exalimi  36606  bj-cbvalimt  36612  bj-eximcom  36616  bj-ssbid1ALT  36638  bj-sb  36660  bj-snsetex  36936  bj-restpw  37065  bj-finsumval0  37258  mptsnunlem  37311  icoreclin  37330  relowlpssretop  37337  inunissunidif  37348  rdgssun  37351  finorwe  37355  domalom  37377  wl-dral1d  37504  wl-exeq  37507  wl-lem-exsb  37539  poimirlem29  37628  poimirlem32  37631  fdc  37724  seqpo  37726  incsequz  37727  isismty  37780  ismtybndlem  37785  heibor1lem  37788  ismgmOLD  37829  isexid2  37834  ghomco  37870  pridlc  38050  relcnveq3  38294  elrelscnveq3  38467  cdleme18d  40274  tendovalco  40744  cdlemn11pre  41189  dihord2pre  41204  indstrd  42166  unitscyglem3  42170  nnadddir  42243  eu6w  42649  incssnn0  42684  fphpd  42789  jm2.19lem3  42964  setindtr  42997  islssfg2  43044  mpaaeu  43123  ordnexbtwnsuc  43240  oaabsb  43267  succlg  43301  oacl2g  43303  omabs2  43305  omcl2  43306  omcl3g  43307  pr2cv  43521  refimssco  43580  iunrelexpmin1  43681  iunrelexpmin2  43685  trclimalb2  43699  clsk1indlem3  44016  tfindsd  44183  mnurndlem1  44254  nzss  44290  sb5ALT  44499  truniALT  44515  ee223  44608  3orbi123VD  44823  sbc3orgVD  44824  exbirVD  44826  exbiriVD  44827  sbcim2gVD  44848  trsbcVD  44850  truniALTVD  44851  onfrALTlem3VD  44860  onfrALTlem2VD  44862  csbrngVD  44869  19.41rgVD  44875  ax6e2eqVD  44880  ax6e2ndeqVD  44882  2uasbanhVD  44884  sb5ALTVD  44886  vk15.4jVD  44887  infxrunb3rnmpt  45408  stoweidlem26  46008  et-equeucl  46854  hirstL-ax3  46877  rexsb  47084  rexrsb  47085  euoreqb  47094  2reu8i  47098  afvres  47157  tz6.12-afv  47158  afvco2  47161  afv2orxorb  47213  afv2res  47224  tz6.12-afv2  47225  tz6.12i-afv2  47228  dfatcolem  47240  zm1nn  47287  2ffzoeq  47312  smonoord  47356  iccpartiltu  47407  iccpartlt  47409  iccpartltu  47410  iccpartgtl  47411  iccpartgt  47412  iccpartleu  47413  iccpartgel  47414  icceuelpart  47421  iccpartnel  47423  lswn0  47429  ichnreuop  47457  ichreuopeq  47458  prsprel  47472  sprsymrelfvlem  47475  sprsymrelf1lem  47476  sprsymrelfolem2  47478  prproropf1olem4  47491  paireqne  47496  prprelb  47501  reupr  47507  goldbachth  47532  odz2prm2pw  47548  fmtno4prmfac  47557  fmtno4prmfac193  47558  prmdvdsfmtnof1lem2  47570  2pwp1prmfmtno  47575  lighneallem2  47591  lighneallem4b  47594  lighneallem4  47595  requad2  47608  odd2prm2  47703  mogoldbblem  47705  gbepos  47743  gbowgt5  47747  gbowge7  47748  stgoldbwt  47761  sbgoldbwt  47762  sbgoldbst  47763  sbgoldbaltlem1  47764  sbgoldbalt  47766  sbgoldbo  47772  nnsum3primesle9  47779  nnsum4primesodd  47781  nnsum4primesoddALTV  47782  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  bgoldbtbndlem1  47790  bgoldbtbndlem2  47791  bgoldbtbndlem3  47792  bgoldbtbnd  47794  dfnbgr6  47842  isuspgrimlem  47880  uhgrimisgrgric  47916  clnbgrgrim  47919  usgrgrtrirex  47935  isubgr3stgrlem4  47954  grilcbri2  47996  grlicsym  47998  grlictr  48000  gricgrlic  48003  gpgvtxedg0  48048  gpgvtxedg1  48049  gpgedg2ov  48051  gpgedg2iv  48052  pgnioedg1  48093  pgnioedg2  48094  pgnioedg3  48095  pgnioedg4  48096  pgnioedg5  48097  pgnbgreunbgrlem2lem3  48101  pgnbgreunbgrlem3  48103  pgnbgreunbgrlem5lem1  48105  pgnbgreunbgrlem5lem2  48106  pgnbgreunbgrlem5lem3  48107  pgnbgreunbgrlem6  48109  upgrwlkupwlk  48125  uspgrsprf1  48132  lmod0rng  48214  lidldomn1  48216  rngccatidALTV  48257  rngcinvALTV  48261  rhmsubcALTVlem4  48269  funcringcsetcALTV2lem9  48283  ringccatidALTV  48291  ringcbasbasALTV  48297  ztprmneprm  48332  pgrpgt2nabl  48351  lmodvsmdi  48364  ply1mulgsumlem2  48373  lincsumcl  48417  ellcoellss  48421  linindslinci  48434  islinindfis  48435  lincext3  48442  lindslinindimp2lem4  48447  lindslinindsimp2lem5  48448  lindslinindsimp2  48449  lindsrng01  48454  ldepspr  48459  lincresunit3lem1  48465  elfzolborelfzop1  48505  dignn0ldlem  48588  nn0sumshdiglem1  48607  1arymaptf1  48628  2arymaptf1  48639  rrx2xpref1o  48704  rrx2plord2  48708  rrx2plordisom  48709  line2ylem  48737  line2xlem  48739  line2y  48741  itschlc0xyqsol1  48752  inlinecirc02plem  48772  fullthinc  49436  tfis2d  49666  onsetrec  49694