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  191  syl5ibcom  244  syl5ibrcom  246  pm5.501  367  impcom  409  impd  412  expcom  415  expdcom  416  simplbi2com  504  imdistanri  571  syldbl2  840  jaod  858  orel1  888  pm2.62  899  pm2.75  933  pm2.64  941  ccased  1038  dedlem0b  1044  3impd  1349  3expd  1354  mp3an1i  1455  minimp  1624  meredith  1644  19.35  1881  speimfw  1968  equtrr  2026  equeucl  2028  sbiedw  2310  cbv1v  2333  exsb  2356  cbv1  2402  ax12b  2424  axc11n  2426  dvelimdf  2449  equvel  2456  dfsb1  2481  sbied  2503  dfmoeu  2531  mo3  2559  mo4  2561  2mo  2645  2eu6  2653  exists2  2658  pm2.61dne  3029  rexlimdv  3154  r19.21v  3180  r19.12  3312  r19.12OLD  3313  2gencl  3517  3gencl  3518  vtocl2ga  3567  rspccv  3610  ceqex  3640  mob  3713  euind  3720  reuind  3749  2reu1  3891  sseq2  4008  nelss  4047  rexdifi  4145  reupick2  4320  rspn0OLD  4353  disjeq0  4455  uneqdifeq  4492  sspw  4613  ssprsseq  4828  preq12b  4851  prnebg  4856  prel12g  4864  3elpr2eq  4907  iinss2  5060  trintss  5284  dtruALT2  5368  reusv2lem1  5396  alxfr  5405  ralxfrALT  5413  exexneq  5434  dtruOLD  5441  copsexgw  5490  copsexg  5491  snopeqop  5506  propeqop  5507  opthhausdorff  5517  opthhausdorff0  5518  poclOLD  5596  pofun  5606  solin  5613  frss  5643  2optocl  5770  3optocl  5771  ssrel  5781  ssrelOLD  5782  ssrel2  5784  ssrelrel  5795  relop  5849  dfres3  5985  asymref2  6116  xpidtr  6121  trin2  6122  poltletr  6131  xp11  6172  relcnvtrg  6263  reuop  6290  tz7.7  6388  ordtr2  6406  suc11  6469  iotavalOLD  6515  funmoOLD  6562  fundif  6595  fss  6732  f0dom0  6773  fv3  6907  tz6.12i  6917  mpteqb  7015  fveqdmss  7078  eldmrexrnb  7091  funopsn  7143  funsndifnop  7146  tpres  7199  funfvima  7229  fvclss  7238  f1veqaeq  7253  isoselem  7335  oprabv  7466  ovg  7569  elovmpt3rab1  7663  sorpsscmpl  7721  iunpw  7755  trom  7861  limom  7868  peano5  7881  peano5OLD  7882  focdmex  7939  funelss  8030  funeldmdif  8031  bropopvvv  8073  bropfvvvvlem  8074  f1o2ndf1  8105  poxp  8111  soxp  8112  poxp2  8126  frxp2  8127  frxp3  8134  suppimacnv  8156  ressuppss  8165  ressuppssdif  8167  tposfn2  8230  wfr3g  8304  onnseq  8341  smoel  8357  smogt  8364  smoiso2  8366  tfr3  8396  tz7.48-2  8439  tz7.48-3  8441  tz7.49  8442  oecl  8534  oaordex  8555  oalimcl  8557  oaass  8558  omordi  8563  omlimcl  8575  odi  8576  omeulem1  8579  oen0  8583  nnawordi  8618  nnaass  8619  nnmordi  8628  omabs  8647  omsmolem  8653  naddssim  8681  iiner  8780  2ecoptocl  8799  3ecoptocl  8800  undifixp  8925  xpdom2  9064  xpf1o  9136  infensuc  9152  findcard2  9161  php  9207  phpOLD  9219  onomeneqOLD  9226  isinf  9257  isinfOLD  9258  findcard2OLD  9281  unblem2  9293  infssuni  9340  finsschain  9356  fsuppunfi  9380  fsuppunbi  9381  marypha1  9426  hartogs  9536  card2on  9546  card2inf  9547  xpwdomg  9577  elirrv  9588  en3lp  9606  preleqg  9607  inf3lem1  9620  inf3lem2  9621  inf3lem3  9622  inf3lem5  9624  noinfep  9652  ttrclss  9712  ttrclselem2  9718  trcl  9720  tcel  9737  frr3g  9748  rankonidlem  9820  scottex  9877  djuunxp  9913  eldju2ndl  9916  updjud  9926  dif1card  10002  fodomnum  10049  cardaleph  10081  kmlem9  10150  kmlem13  10154  cflim2  10255  cfsmolem  10262  infpssrlem3  10297  isfin7-2  10388  fin1a2lem6  10397  fin1a2lem12  10403  domtriomlem  10434  axdc3lem4  10445  axdc4lem  10447  zorn2lem3  10490  zorn2lem4  10491  zorn2lem5  10492  zorn2lem7  10494  zornn0g  10497  axdclem2  10512  ondomon  10555  alephval2  10564  cfpwsdom  10576  wuncval2  10739  grupr  10789  gruiun  10791  ingru  10807  grothomex  10821  indpi  10899  nqereu  10921  prlem934  11025  reclem2pr  11040  mulgt0sr  11097  supsrlem  11103  dedekind  11374  lemul1a  12065  squeeze0  12114  peano5nni  12212  nnunb  12465  nn0lt2  12622  nn0le2is012  12623  fzind  12657  nn0ind-raph  12659  zindd  12660  eluzaddOLD  12854  uzin  12859  nn01to3  12922  xnn0xadd0  13223  xmulasslem  13261  icoshft  13447  fzen  13515  uzsubsubfz  13520  elfz0ubfz0  13602  elfz0fzfz0  13603  fz0fzelfz0  13604  elfzmlbp  13609  elfzodifsumelfzo  13695  ssfzo12bi  13724  elfzonelfzo  13731  elfznelfzo  13734  injresinjlem  13749  injresinj  13750  modfzo0difsn  13905  modsumfzodifsn  13906  addmodlteq  13908  ssnn0fi  13947  fsuppmapnn0fiub0  13955  expcllem  14035  expeq0  14055  mulexp  14064  leexp2r  14136  bernneq  14189  facdiv  14244  hasheqf1oi  14308  hashnn0n0nn  14348  hashss  14366  hashgt12el  14379  hashgt12el2  14380  hashimarni  14398  hashle2pr  14435  pr2pwpr  14437  hashge2el2dif  14438  hashge2el2difr  14439  hashtpg  14443  hashge3el3dif  14444  exprelprel  14447  hash1to3  14449  fundmge2nop0  14450  fi1uzind  14455  ccatsymb  14529  swrdnd  14601  swrdnd2  14602  swrdnnn0nd  14603  swrdnd0  14604  pfxnd0  14635  swrdswrdlem  14651  swrdswrd  14652  pfxccatin12lem2a  14674  pfxccatin12lem1  14675  swrdccatin2  14676  pfxccatin12lem2  14678  pfxccatin12lem3  14679  pfxccat3  14681  swrdccat  14682  swrdccat3blem  14686  repsdf2  14725  repswswrd  14731  cshwidxmod  14750  cshwidx0  14753  cshf1  14757  cshweqrep  14768  cshw1  14769  cshwsexaOLD  14772  2cshwcshw  14773  scshwfzeqfzo  14774  cshwcsh2id  14776  wwlktovfo  14906  relexpaddg  14997  iseraltlem2  15626  modfsummods  15736  clim2prod  15831  prodfn0  15837  prodfrec  15838  prodmo  15877  fprodabs  15915  binomfallfac  15982  fprodefsum  16035  dvdsaddre2b  16247  addmodlteqALT  16265  oddge22np1  16289  nn0enne  16317  nn0o1gt2  16321  sumeven  16327  sumodd  16328  dvdslegcd  16442  gcdneg  16460  dfgcd2  16485  rplpwr  16496  lcmf  16567  lcmftp  16570  lcmfunsnlem2lem1  16572  lcmfunsnlem2  16574  lcmfdvdsb  16577  coprmdvds1  16586  qredeq  16591  coprmprod  16595  coprmproddvdslem  16596  cncongr1  16601  cncongr2  16602  prm2orodd  16625  2mulprm  16627  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  17026  cshwshashlem2  17027  cshwshashlem3  17028  cshwrepswhash1  17033  setsn0fun  17103  setsstruct2  17104  imasleval  17484  mreiincl  17537  mreexexd  17589  inveq  17718  cicsym  17748  cictr  17749  initoid  17948  termoid  17949  initoeu2lem0  17960  initoeu2lem1  17961  initoeu2lem2  17962  initoeu2  17963  fthestrcsetc  18099  fthsetcestrc  18114  drsdirfi  18255  isnmgm  18562  sgrpass  18613  insubm  18696  mgm2nsgrplem3  18798  dfgrp3lem  18918  cyccom  19075  symg2bas  19255  symgfix2  19279  symgextf1  19284  gsmsymgrfix  19291  pmtrprfv3  19317  psgnunilem4  19360  efgi2  19588  0ringnnzr  20295  psgndiflemB  21145  psgndiflemA  21146  elfrlmbasn0  21310  lmictra  21392  mpfrcl  21640  gsummoncoe1  21820  mamufacex  21883  matecl  21919  dmatelnd  21990  dmatscmcl  21997  scmateALT  22006  scmatsgrp1  22016  scmatf1  22025  mavmulsolcl  22045  cramerimplem1  22177  cramerimplem2  22178  pmatcollpw3fi1  22282  mp2pm2mplem4  22303  pm2mpfo  22308  chmaidscmat  22342  fvmptnn04ifb  22345  chfacfscmul0  22352  chfacfpmmul0  22356  cayhamlem1  22360  cayhamlem3  22381  cayleyhamilton1  22386  fiinopn  22395  tgcl  22464  distop  22490  isclo2  22584  iscldtop  22591  ssnei2  22612  opnnei  22616  pnfnei  22716  mnfnei  22717  tgcnp  22749  cnpnei  22760  1stcelcls  22957  txcnpi  23104  cnmptcom  23174  fbfinnfr  23337  isfildlem  23353  snfil  23360  fbunfip  23365  fgcl  23374  elfm2  23444  fmco  23457  fbflim2  23473  cnpflf2  23496  flimfcls  23522  tmdgsum  23591  neibl  24002  tngngpim  24168  fgcfil  24780  caubl  24817  volsuplem  25064  ellimc3  25388  dvnadd  25438  dvnres  25440  cpnord  25444  dvnfre  25461  ply1divex  25646  cxpmul2  26189  zabsle1  26789  gausslemma2dlem1a  26858  gausslemma2dlem3  26861  lgsquad2lem2  26878  2lgs  26900  2sq2  26926  2sqnn0  26931  2sqnn  26932  2sqreultlem  26940  2sqreunnltlem  26943  qabvexp  27119  sltval2  27149  nolt02o  27188  ssltun1  27299  scutun12  27301  madebday  27384  mulsprop  27576  precsexlem8  27650  precsexlem9  27651  axcontlem4  28215  umgredgprv  28357  umgrnloop  28358  upgrpredgv  28389  upgredgpr  28392  edglnl  28393  usgredgprvALT  28442  usgrnloopALT  28450  usgredg2v  28474  fusgrfis  28577  nbuhgr2vtx1edgblem  28598  nb3grprlem1  28627  cusgrsize2inds  28700  cusgrfi  28705  fusgrn0degnn0  28746  uspgrloopvtxel  28763  vtxdginducedm1lem4  28789  uhgr0edg0rgrb  28821  wlkl1loop  28885  wlk1walk  28886  upgriswlk  28888  upgrwlkvtxedg  28892  uspgr2wlkeq  28893  wlkv0  28898  wlksoneq1eq2  28911  wlkon2n0  28913  wlkreslem  28916  wlkres  28917  lfgrwlkprop  28934  pthdivtx  28976  2pthnloop  28978  spthonepeq  28999  uhgrwkspthlem2  29001  uhgrwkspth  29002  usgr2wlkneq  29003  usgr2trlncl  29007  usgr2pthlem  29010  usgr2pth  29011  cyclnspth  29047  lfgrn1cycl  29049  usgr2trlncrct  29050  uspgrn2crct  29052  crctcshwlkn0lem3  29056  crctcshwlkn0lem5  29058  wwlknp  29087  wspthneq1eq2  29104  0enwwlksnge1  29108  wlklnwwlkln1  29112  wlkiswwlks2  29119  wlkiswwlksupgr2  29121  wlklnwwlkln2lem  29126  wwlksnred  29136  wwlksnextbi  29138  wwlksnredwwlkn0  29140  wwlksnextwrd  29141  wwlksnextinj  29143  wwlksnextproplem3  29155  wwlksnextprop  29156  wspthsnwspthsnon  29160  wspthsnonn0vne  29161  2pthon3v  29187  umgr2adedgwlkonALT  29191  umgr2wlk  29193  umgr2wlkon  29194  umgrwwlks2on  29201  elwspths2on  29204  usgr2wspthons3  29208  elwwlks2  29210  rusgrnumwwlk  29219  clwwlkccatlem  29232  clwlkclwwlklem2a4  29240  clwlkclwwlklem2a  29241  clwlkclwwlklem2  29243  clwlkclwwlkf1lem3  29249  erclwwlkeqlen  29262  clwwlknwwlksn  29281  loopclwwlkn1b  29285  clwwlkf1  29292  wwlksext2clwwlk  29300  eleclclwwlknlem2  29304  umgr2cwwk2dif  29307  eleclclwwlkn  29319  hashecclwwlkn1  29320  umgrhashecclwwlk  29321  clwwlknonwwlknonb  29349  clwwlknonex2lem2  29351  clwwlknonex2  29352  1pthon2v  29396  upgr3v3e3cycl  29423  uhgr3cyclexlem  29424  uhgr3cyclex  29425  eupth2lem3lem4  29474  frgr3vlem1  29516  frgr3vlem2  29517  3vfriswmgrlem  29520  3vfriswmgr  29521  3cyclfrgrrn1  29528  n4cyclfrgr  29534  frgrncvvdeqlem3  29544  frgrncvvdeqlem6  29547  frgrncvvdeqlem7  29548  frgrncvvdeqlem8  29549  frgrwopreglem4a  29553  frgrwopreglem3  29557  frgrwopreg1  29561  frgrwopreg2  29562  frgrwopreglem5lem  29563  frgrwopreglem5ALT  29565  frgrwopreg  29566  fusgr2wsp2nb  29577  2wspmdisj  29580  numclwwlk1lem2foa  29597  numclwwlk1lem2f1  29600  numclwwlk1lem2fo  29601  numclwwlk1  29604  wlkl0  29610  numclwwlk2lem1  29619  numclwlk2lem2f  29620  numclwlk2lem2f1o  29622  frgrreg  29637  frgrregord013  29638  frgrregord13  29639  friendshipgt3  29641  friendship  29642  eulplig  29726  ipassi  30082  ubthlem2  30112  isch3  30482  shintcli  30570  shmodsi  30630  spansncvi  30893  hoaddsub  31057  eigorthi  31078  pjss2coi  31405  pjnormssi  31409  pj3cor1i  31450  strb  31499  dmdmd  31541  mdsl0  31551  csmdsymi  31575  chrelat2i  31606  mdsymlem3  31646  mdsymlem6  31649  sumdmdlem2  31660  opreu2reuALT  31705  ssrelf  31832  spthcycl  34109  loop1cycl  34117  cvmlift2lem1  34282  satfrel  34347  satfrnmapom  34350  fmlafvel  34365  fmla1  34367  gonarlem  34374  gonar  34375  goalrlem  34376  goalr  34377  satffunlem  34381  satffunlem1lem1  34382  satffunlem2lem1  34384  satffun  34389  satefvfmla1  34405  mrsubvrs  34502  mclsax  34549  3ccased  34677  dfon2lem3  34746  rdgprc  34755  cgrextend  34969  btwndiff  34988  btwnconn1lem12  35059  brsegle  35069  broutsideof2  35083  funray  35101  elicc3  35191  nn0prpwlem  35196  nn0prpw  35197  fnessref  35231  neibastop2lem  35234  filnetlem4  35255  meran1  35285  waj-ax  35288  arg-ax  35290  bj-nnclavc  35413  bj-con2com  35426  bj-axdd2  35459  bj-alrimg  35485  bj-exlimg  35489  bj-exalimi  35499  bj-cbvalimt  35505  bj-eximcom  35509  bj-ssbid1ALT  35531  bj-sb  35554  bj-snsetex  35833  bj-restpw  35962  bj-finsumval0  36155  mptsnunlem  36208  icoreclin  36227  relowlpssretop  36234  inunissunidif  36245  rdgssun  36248  finorwe  36252  domalom  36274  wl-dral1d  36389  wl-exeq  36392  wl-lem-exsb  36420  poimirlem29  36506  poimirlem32  36509  fdc  36602  seqpo  36604  incsequz  36605  isismty  36658  ismtybndlem  36663  heibor1lem  36666  ismgmOLD  36707  isexid2  36712  ghomco  36748  pridlc  36928  relcnveq3  37179  elrelscnveq3  37350  cdleme18d  39155  tendovalco  39625  cdlemn11pre  40070  dihord2pre  40085  nnadddir  41182  incssnn0  41435  fphpd  41540  jm2.19lem3  41716  setindtr  41749  islssfg2  41799  mpaaeu  41878  ordnexbtwnsuc  42003  oaabsb  42030  succlg  42064  oacl2g  42066  omabs2  42068  omcl2  42069  omcl3g  42070  pr2cv  42285  refimssco  42344  iunrelexpmin1  42445  iunrelexpmin2  42449  trclimalb2  42463  clsk1indlem3  42780  tfindsd  42950  mnurndlem1  43026  nzss  43062  sb5ALT  43272  truniALT  43288  ee223  43381  3orbi123VD  43597  sbc3orgVD  43598  exbirVD  43600  exbiriVD  43601  sbcim2gVD  43622  trsbcVD  43624  truniALTVD  43625  onfrALTlem3VD  43634  onfrALTlem2VD  43636  csbrngVD  43643  19.41rgVD  43649  ax6e2eqVD  43654  ax6e2ndeqVD  43656  2uasbanhVD  43658  sb5ALTVD  43660  vk15.4jVD  43661  infxrunb3rnmpt  44125  stoweidlem26  44729  et-equeucl  45575  hirstL-ax3  45589  rexsb  45794  rexrsb  45795  euoreqb  45804  2reu8i  45808  afvres  45867  tz6.12-afv  45868  afvco2  45871  afv2orxorb  45923  afv2res  45934  tz6.12-afv2  45935  tz6.12i-afv2  45938  dfatcolem  45950  zm1nn  45997  fzoopth  46022  2ffzoeq  46023  smonoord  46026  iccpartiltu  46077  iccpartlt  46079  iccpartltu  46080  iccpartgtl  46081  iccpartgt  46082  iccpartleu  46083  iccpartgel  46084  icceuelpart  46091  iccpartnel  46093  lswn0  46099  ichnreuop  46127  ichreuopeq  46128  prsprel  46142  sprsymrelfvlem  46145  sprsymrelf1lem  46146  sprsymrelfolem2  46148  prproropf1olem4  46161  paireqne  46166  prprelb  46171  reupr  46177  goldbachth  46202  odz2prm2pw  46218  fmtno4prmfac  46227  fmtno4prmfac193  46228  prmdvdsfmtnof1lem2  46240  2pwp1prmfmtno  46245  lighneallem2  46261  lighneallem4b  46264  lighneallem4  46265  requad2  46278  odd2prm2  46373  mogoldbblem  46375  gbepos  46413  gbowgt5  46417  gbowge7  46418  stgoldbwt  46431  sbgoldbwt  46432  sbgoldbst  46433  sbgoldbaltlem1  46434  sbgoldbalt  46436  sbgoldbo  46442  nnsum3primesle9  46449  nnsum4primesodd  46451  nnsum4primesoddALTV  46452  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  bgoldbtbndlem1  46460  bgoldbtbndlem2  46461  bgoldbtbndlem3  46462  bgoldbtbnd  46464  isomuspgrlem1  46482  upgrwlkupwlk  46505  uspgrsprf1  46512  mgmhmlin  46543  issubmgm2  46547  lmod0rng  46629  rngqiprngimfo  46767  lidldomn1  46777  rnghmsscmap  46826  rnghmsubcsetclem2  46828  rngcinv  46833  rngccatidALTV  46841  rngcinvALTV  46845  funcrngcsetc  46850  funcrngcsetcALT  46851  rhmsscmap  46872  rhmsubcsetclem2  46874  rhmsubcrngclem2  46880  ringcbasbas  46886  funcringcsetc  46887  funcringcsetcALTV2lem9  46896  ringccatidALTV  46904  ringcbasbasALTV  46910  rhmsubclem4  46941  rhmsubcALTVlem4  46959  ztprmneprm  46977  pgrpgt2nabl  46996  lmodvsmdi  47012  ply1mulgsumlem2  47022  lincsumcl  47066  ellcoellss  47070  linindslinci  47083  islinindfis  47084  lincext3  47091  lindslinindimp2lem4  47096  lindslinindsimp2lem5  47097  lindslinindsimp2  47098  lindsrng01  47103  ldepspr  47108  lincresunit3lem1  47114  elfzolborelfzop1  47154  dignn0ldlem  47242  nn0sumshdiglem1  47261  1arymaptf1  47282  2arymaptf1  47293  rrx2xpref1o  47358  rrx2plord2  47362  rrx2plordisom  47363  line2ylem  47391  line2xlem  47393  line2y  47395  itschlc0xyqsol1  47406  inlinecirc02plem  47426  fullthinc  47620  tfis2d  47679  onsetrec  47707