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  842  jaod  860  orel1  889  pm2.62  900  pm2.75  934  pm2.64  944  ccased  1039  dedlem0b  1045  3impd  1350  3expd  1355  mp3an1i  1457  minimp  1623  meredith  1643  19.35  1879  speimfw  1965  equtrr  2024  equeucl  2026  ax12ev2  2188  sbiedw  2322  cbv1v  2341  exsb  2364  cbv1  2407  ax12b  2429  axc11n  2431  dvelimdf  2454  equvel  2461  dfsb1  2486  sbied  2508  dfmoeu  2536  mo3  2565  mo4  2567  2mo  2649  2eu6  2658  exists2  2663  pm2.61dne  3019  rexlimdv  3137  r19.21v  3163  r19.12  3287  2gencl  3485  3gencl  3486  vtocl2ga  3535  vtocl2gaf  3536  vtocl3gaf  3538  vtocl3ga  3540  vtocl4ga  3543  rspccv  3575  ceqex  3608  mob  3677  euind  3684  reuind  3713  2reu1  3849  sseq2  3962  nelss  4001  rexdifi  4104  reupick2  4285  disjeq0  4410  uneqdifeq  4447  sspw  4567  ssprsseq  4783  preq12b  4808  prnebg  4814  prel12g  4822  3elpr2eq  4864  iinss2  5015  trintss  5225  dtruALT2  5317  reusv2lem1  5345  alxfr  5354  ralxfrALT  5362  exexneq  5391  copsexgw  5446  copsexg  5447  snopeqop  5462  propeqop  5463  opthhausdorff  5473  opthhausdorff0  5474  pofun  5558  solin  5567  frss  5596  2optocl  5728  3optocl  5729  ssrel  5740  ssrel2  5742  ssrelrel  5753  relop  5807  dfres3  5951  asymref2  6082  xpidtr  6087  trin2  6088  poltletr  6097  imadifssran  6117  xp11  6141  relcnvtrg  6233  reuop  6259  tz7.7  6351  ordtr2  6370  suc11  6434  fundif  6549  fss  6686  f0dom0  6726  fv3  6860  tz6.12i  6868  mpteqb  6969  fveqdmss  7032  eldmrexrnb  7046  funopsn  7103  funsndifnop  7106  tpres  7157  funfvima  7186  fvclss  7197  f1veqaeq  7212  fvf1pr  7263  isoselem  7297  oprabv  7428  ovg  7533  elovmpt3rab1  7628  sorpsscmpl  7689  iunpw  7726  trom  7827  limom  7834  peano5  7845  focdmex  7910  funelss  8001  funeldmdif  8002  bropopvvv  8042  bropfvvvvlem  8043  f1o2ndf1  8074  poxp  8080  soxp  8081  poxp2  8095  frxp2  8096  frxp3  8103  suppimacnv  8126  ressuppss  8135  ressuppssdif  8137  tposfn2  8200  wfr3g  8271  onnseq  8286  smoel  8302  smogt  8309  smoiso2  8311  tfr3  8340  tz7.48-2  8383  tz7.48-3  8385  tz7.49  8386  oecl  8474  oaordex  8495  oalimcl  8497  oaass  8498  omordi  8503  omlimcl  8515  odi  8516  omeulem1  8519  oen0  8524  nnawordi  8559  nnaass  8560  nnmordi  8569  omabs  8589  omsmolem  8595  naddssim  8623  brinxper  8675  iiner  8738  2ecoptocl  8757  3ecoptocl  8758  undifixp  8884  xpdom2  9012  xpf1o  9079  infensuc  9095  findcard2  9101  php  9143  isinf  9177  unblem2  9205  fodomfir  9240  infssuni  9258  finsschain  9271  fsuppunfi  9303  fsuppunbi  9304  marypha1  9349  hartogs  9461  card2on  9471  card2inf  9472  xpwdomg  9502  elirrv  9514  elirrvOLD  9515  en3lp  9535  preleqg  9536  inf3lem1  9549  inf3lem2  9550  inf3lem3  9551  inf3lem5  9553  noinfep  9581  ttrclss  9641  ttrclselem2  9647  trcl  9649  tcel  9664  frr3g  9680  rankonidlem  9752  scottex  9809  djuunxp  9845  eldju2ndl  9848  updjud  9858  dif1card  9932  fodomnum  9979  cardaleph  10011  kmlem9  10081  kmlem13  10085  cflim2  10185  cfsmolem  10192  infpssrlem3  10227  isfin7-2  10318  fin1a2lem6  10327  fin1a2lem12  10333  domtriomlem  10364  axdc3lem4  10375  axdc4lem  10377  zorn2lem3  10420  zorn2lem4  10421  zorn2lem5  10422  zorn2lem7  10424  zornn0g  10427  axdclem2  10442  ondomon  10485  alephval2  10495  cfpwsdom  10507  wuncval2  10670  grupr  10720  gruiun  10722  ingru  10738  grothomex  10752  indpi  10830  nqereu  10852  prlem934  10956  reclem2pr  10971  mulgt0sr  11028  supsrlem  11034  1re  11144  dedekind  11308  lemul1a  12007  squeeze0  12057  peano5nni  12160  nnunb  12409  nn0lt2  12567  nn0le2is012  12568  fzind  12602  nn0ind-raph  12604  zindd  12605  uzin  12799  nn01to3  12866  xnn0xadd0  13174  xmulasslem  13212  icoshft  13401  fzen  13469  uzsubsubfz  13474  elfz0ubfz0  13560  elfz0fzfz0  13561  fz0fzelfz0  13562  elfzmlbp  13567  elfzodifsumelfzo  13659  ssfzo12bi  13689  fzoopth  13690  elfzonelfzo  13697  elfznelfzo  13701  injresinjlem  13718  injresinj  13719  modfzo0difsn  13878  modsumfzodifsn  13879  addmodlteq  13881  ssnn0fi  13920  fsuppmapnn0fiub0  13928  expcllem  14007  expeq0  14027  mulexp  14036  leexp2r  14109  bernneq  14164  facdiv  14222  hasheqf1oi  14286  hashnn0n0nn  14326  hashss  14344  hashgt12el  14357  hashgt12el2  14358  hashimarni  14376  hashle2pr  14412  pr2pwpr  14414  hashge2el2dif  14415  hashge2el2difr  14416  hashtpg  14420  hashge3el3dif  14422  exprelprel  14425  hash1to3  14427  hash3tpde  14428  tpfo  14435  fundmge2nop0  14437  fi1uzind  14442  ccatsymb  14518  swrdnd  14590  swrdnd2  14591  swrdnnn0nd  14592  swrdnd0  14593  pfxnd0  14624  swrdswrdlem  14639  swrdswrd  14640  pfxccatin12lem2a  14662  pfxccatin12lem1  14663  swrdccatin2  14664  pfxccatin12lem2  14666  pfxccatin12lem3  14667  pfxccat3  14669  swrdccat  14670  swrdccat3blem  14674  repsdf2  14713  repswswrd  14719  cshwidxmod  14738  cshwidx0  14741  cshf1  14745  cshweqrep  14756  cshw1  14757  2cshwcshw  14760  scshwfzeqfzo  14761  cshwcsh2id  14763  wwlktovfo  14893  relexpaddg  14988  iseraltlem2  15618  modfsummods  15728  clim2prod  15823  prodfn0  15829  prodfrec  15830  prodmo  15871  fprodabs  15909  binomfallfac  15976  fprodefsum  16030  dvdsaddre2b  16246  addmodlteqALT  16264  oddge22np1  16288  nn0enne  16316  nn0o1gt2  16320  sumeven  16326  sumodd  16327  dvdslegcd  16443  gcdneg  16461  dfgcd2  16485  rplpwr  16497  lcmf  16572  lcmftp  16575  lcmfunsnlem2lem1  16577  lcmfunsnlem2  16579  lcmfdvdsb  16582  coprmdvds1  16591  qredeq  16596  coprmprod  16600  coprmproddvdslem  16601  cncongr1  16606  cncongr2  16607  prm2orodd  16630  2mulprm  16632  nnnn0modprm0  16746  prm23lt5  16754  prm23ge5  16755  dvdsprmpweqnn  16825  dvdsprmpweqle  16826  oddprmdvds  16843  prmpwdvds  16844  prmreclem4  16859  ramcl  16969  prmgaplem6  16996  prmgaplem7  16997  prmgaplem8  16998  cshwshashlem1  17035  cshwshashlem2  17036  cshwshashlem3  17037  cshwrepswhash1  17042  setsn0fun  17112  setsstruct2  17113  imasleval  17474  mreiincl  17527  mreexexd  17583  inveq  17710  cicsym  17740  cictr  17741  initoid  17937  termoid  17938  initoeu2lem0  17949  initoeu2lem1  17950  initoeu2lem2  17951  initoeu2  17952  fthestrcsetc  18085  fthsetcestrc  18100  drsdirfi  18240  isnmgm  18581  mgmhmlin  18636  issubmgm2  18640  sgrpass  18662  insubm  18755  mgm2nsgrplem3  18857  dfgrp3lem  18980  cyccom  19144  symg2bas  19334  symgfix2  19357  symgextf1  19362  gsmsymgrfix  19369  pmtrprfv3  19395  psgnunilem4  19438  efgi2  19666  0ringnnzr  20470  rnghmsscmap  20575  rnghmsubcsetclem2  20577  rngcinv  20582  funcrngcsetc  20585  funcrngcsetcALT  20586  rhmsscmap  20604  rhmsubcsetclem2  20606  rhmsubcrngclem2  20612  ringcbasbas  20618  funcringcsetc  20619  rhmsubclem4  20633  rngqiprngimfo  21268  psgndiflemB  21567  psgndiflemA  21568  elfrlmbasn0  21730  lmictra  21812  mpfrcl  22052  gsummoncoe1  22264  mamufacex  22352  matecl  22381  dmatelnd  22452  dmatscmcl  22459  scmateALT  22468  scmatsgrp1  22478  scmatf1  22487  mavmulsolcl  22507  cramerimplem1  22639  cramerimplem2  22640  pmatcollpw3fi1  22744  mp2pm2mplem4  22765  pm2mpfo  22770  chmaidscmat  22804  fvmptnn04ifb  22807  chfacfscmul0  22814  chfacfpmmul0  22818  cayhamlem1  22822  cayhamlem3  22843  cayleyhamilton1  22848  fiinopn  22857  tgcl  22925  distop  22951  isclo2  23044  iscldtop  23051  ssnei2  23072  opnnei  23076  pnfnei  23176  mnfnei  23177  tgcnp  23209  cnpnei  23220  1stcelcls  23417  txcnpi  23564  cnmptcom  23634  fbfinnfr  23797  isfildlem  23813  snfil  23820  fbunfip  23825  fgcl  23834  elfm2  23904  fmco  23917  fbflim2  23933  cnpflf2  23956  flimfcls  23982  tmdgsum  24051  neibl  24457  tngngpim  24615  fgcfil  25239  caubl  25276  volsuplem  25524  ellimc3  25848  dvnadd  25899  dvnres  25901  cpnord  25905  dvnfre  25924  ply1divex  26110  cxpmul2  26666  fsumdvdsmul  27173  zabsle1  27275  gausslemma2dlem1a  27344  gausslemma2dlem3  27347  lgsquad2lem2  27364  2lgs  27386  2sq2  27412  2sqnn0  27417  2sqnn  27418  2sqreultlem  27426  2sqreunnltlem  27429  qabvexp  27605  ltsval2  27636  nolt02o  27675  sltsun1  27796  cutsun12  27798  madebday  27908  mulsprop  28138  precsexlem8  28222  precsexlem9  28223  noseqind  28300  om2noseqrdg  28312  n0cutlt  28367  peano5uzs  28412  expadds  28443  bdaypw2n0bndlem  28471  bdaypw2n0bnd  28472  axcontlem4  29052  umgredgprv  29192  umgrnloop  29193  upgrpredgv  29224  upgredgpr  29227  edglnl  29228  usgredgprvALT  29280  usgrnloopALT  29288  usgredg2v  29312  fusgrfis  29415  nbuhgr2vtx1edgblem  29436  nb3grprlem1  29465  cusgrsize2inds  29539  cusgrfi  29544  fusgrn0degnn0  29585  uspgrloopvtxel  29602  vtxdginducedm1lem4  29628  uhgr0edg0rgrb  29660  wlkl1loop  29723  wlk1walk  29724  upgriswlk  29726  upgrwlkvtxedg  29730  uspgr2wlkeq  29731  wlkv0  29735  wlksoneq1eq2  29748  wlkon2n0  29750  wlkreslem  29753  wlkres  29754  lfgrwlkprop  29771  pthdivtx  29812  2pthnloop  29816  spthonepeq  29837  uhgrwkspthlem2  29839  uhgrwkspth  29840  usgr2wlkneq  29841  usgr2trlncl  29845  usgr2pthlem  29848  usgr2pth  29849  cyclnspth  29886  lfgrn1cycl  29890  usgr2trlncrct  29891  uspgrn2crct  29893  crctcshwlkn0lem3  29897  crctcshwlkn0lem5  29899  wwlknp  29928  wspthneq1eq2  29945  0enwwlksnge1  29949  wlklnwwlkln1  29953  wlkiswwlks2  29960  wlkiswwlksupgr2  29962  wlklnwwlkln2lem  29967  wwlksnred  29977  wwlksnextbi  29979  wwlksnredwwlkn0  29981  wwlksnextwrd  29982  wwlksnextinj  29984  wwlksnextproplem3  29996  wwlksnextprop  29997  wspthsnwspthsnon  30001  wspthsnonn0vne  30002  2pthon3v  30028  umgr2adedgwlkonALT  30032  umgr2wlk  30034  umgr2wlkon  30035  usgrwwlks2on  30043  umgrwwlks2on  30044  elwspths2on  30047  elwspths2onw  30048  usgr2wspthons3  30052  elwwlks2  30054  rusgrnumwwlk  30063  clwwlkccatlem  30076  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwlkclwwlklem2  30087  clwlkclwwlkf1lem3  30093  erclwwlkeqlen  30106  clwwlknwwlksn  30125  loopclwwlkn1b  30129  clwwlkf1  30136  wwlksext2clwwlk  30144  eleclclwwlknlem2  30148  umgr2cwwk2dif  30151  eleclclwwlkn  30163  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  clwwlknonwwlknonb  30193  clwwlknonex2lem2  30195  clwwlknonex2  30196  1pthon2v  30240  upgr3v3e3cycl  30267  uhgr3cyclexlem  30268  uhgr3cyclex  30269  eupth2lem3lem4  30318  frgr3vlem1  30360  frgr3vlem2  30361  3vfriswmgrlem  30364  3vfriswmgr  30365  3cyclfrgrrn1  30372  n4cyclfrgr  30378  frgrncvvdeqlem3  30388  frgrncvvdeqlem6  30391  frgrncvvdeqlem7  30392  frgrncvvdeqlem8  30393  frgrwopreglem4a  30397  frgrwopreglem3  30401  frgrwopreg1  30405  frgrwopreg2  30406  frgrwopreglem5lem  30407  frgrwopreglem5ALT  30409  frgrwopreg  30410  fusgr2wsp2nb  30421  2wspmdisj  30424  numclwwlk1lem2foa  30441  numclwwlk1lem2f1  30444  numclwwlk1lem2fo  30445  numclwwlk1  30448  wlkl0  30454  numclwwlk2lem1  30463  numclwlk2lem2f  30464  numclwlk2lem2f1o  30466  frgrreg  30481  frgrregord013  30482  frgrregord13  30483  friendshipgt3  30485  friendship  30486  eulplig  30572  ipassi  30928  ubthlem2  30958  isch3  31328  shintcli  31416  shmodsi  31476  spansncvi  31739  hoaddsub  31903  eigorthi  31924  pjss2coi  32251  pjnormssi  32255  pj3cor1i  32296  strb  32345  dmdmd  32387  mdsl0  32397  csmdsymi  32421  chrelat2i  32452  mdsymlem3  32492  mdsymlem6  32495  sumdmdlem2  32506  opreu2reuALT  32562  ssrelf  32704  gsumwun  33169  r1filim  35279  trssfir1om  35286  fineqvinfep  35300  trssfir1omregs  35311  onvf1odlem4  35319  spthcycl  35342  loop1cycl  35350  cvmlift2lem1  35515  satfrel  35580  satfrnmapom  35583  fmlafvel  35598  fmla1  35600  gonarlem  35607  gonar  35608  goalrlem  35609  goalr  35610  satffunlem  35614  satffunlem1lem1  35615  satffunlem2lem1  35617  satffun  35622  satefvfmla1  35638  mrsubvrs  35735  mclsax  35782  3ccased  35932  dfon2lem3  35996  rdgprc  36005  cgrextend  36221  btwndiff  36240  btwnconn1lem12  36311  brsegle  36321  broutsideof2  36335  funray  36353  in-ax8  36437  ss-ax8  36438  elicc3  36530  nn0prpwlem  36535  nn0prpw  36536  fnessref  36570  neibastop2lem  36573  filnetlem4  36594  meran1  36624  waj-ax  36627  arg-ax  36629  bj-nnclavc  36767  bj-con2com  36782  bj-axdd2  36814  bj-alrimg  36835  bj-exlimg  36855  bj-exalimi  36865  bj-cbvalimt  36872  bj-eximcom  36874  bj-ssbid1ALT  36907  bj-sb  36929  bj-snsetex  37208  bj-axseprep  37319  bj-axreprepsep  37320  bj-restpw  37342  bj-finsumval0  37537  mptsnunlem  37590  icoreclin  37609  relowlpssretop  37616  inunissunidif  37627  rdgssun  37630  finorwe  37634  domalom  37656  wl-dral1d  37783  wl-exeq  37786  wl-lem-exsb  37818  wl-eujustlem1  37840  poimirlem29  37897  poimirlem32  37900  fdc  37993  seqpo  37995  incsequz  37996  isismty  38049  ismtybndlem  38054  heibor1lem  38057  ismgmOLD  38098  isexid2  38103  ghomco  38139  pridlc  38319  relcnveq3  38575  elrelscnveq3  38875  cdleme18d  40668  tendovalco  41138  cdlemn11pre  41583  dihord2pre  41598  indstrd  42560  unitscyglem3  42564  nnadddir  42637  eu6w  43031  incssnn0  43065  fphpd  43170  jm2.19lem3  43345  setindtr  43378  islssfg2  43425  mpaaeu  43504  ordnexbtwnsuc  43621  oaabsb  43648  succlg  43682  oacl2g  43684  omabs2  43686  omcl2  43687  omcl3g  43688  pr2cv  43901  refimssco  43960  iunrelexpmin1  44061  iunrelexpmin2  44065  trclimalb2  44079  clsk1indlem3  44396  tfindsd  44563  mnurndlem1  44634  nzss  44670  sb5ALT  44878  truniALT  44894  ee223  44987  3orbi123VD  45202  sbc3orgVD  45203  exbirVD  45205  exbiriVD  45206  sbcim2gVD  45227  trsbcVD  45229  truniALTVD  45230  onfrALTlem3VD  45239  onfrALTlem2VD  45241  csbrngVD  45248  19.41rgVD  45254  ax6e2eqVD  45259  ax6e2ndeqVD  45261  2uasbanhVD  45263  sb5ALTVD  45265  vk15.4jVD  45266  infxrunb3rnmpt  45783  stoweidlem26  46381  et-equeucl  47227  hirstL-ax3  47249  rexsb  47456  rexrsb  47457  euoreqb  47466  2reu8i  47470  afvres  47529  tz6.12-afv  47530  afvco2  47533  afv2orxorb  47585  afv2res  47596  tz6.12-afv2  47597  tz6.12i-afv2  47600  dfatcolem  47612  zm1nn  47659  2ffzoeq  47684  smonoord  47728  iccpartiltu  47779  iccpartlt  47781  iccpartltu  47782  iccpartgtl  47783  iccpartgt  47784  iccpartleu  47785  iccpartgel  47786  icceuelpart  47793  iccpartnel  47795  lswn0  47801  ichnreuop  47829  ichreuopeq  47830  prsprel  47844  sprsymrelfvlem  47847  sprsymrelf1lem  47848  sprsymrelfolem2  47850  prproropf1olem4  47863  paireqne  47868  prprelb  47873  reupr  47879  goldbachth  47904  odz2prm2pw  47920  fmtno4prmfac  47929  fmtno4prmfac193  47930  prmdvdsfmtnof1lem2  47942  2pwp1prmfmtno  47947  lighneallem2  47963  lighneallem4b  47966  lighneallem4  47967  requad2  47980  odd2prm2  48075  mogoldbblem  48077  gbepos  48115  gbowgt5  48119  gbowge7  48120  stgoldbwt  48133  sbgoldbwt  48134  sbgoldbst  48135  sbgoldbaltlem1  48136  sbgoldbalt  48138  sbgoldbo  48144  nnsum3primesle9  48151  nnsum4primesodd  48153  nnsum4primesoddALTV  48154  nnsum4primeseven  48157  nnsum4primesevenALTV  48158  bgoldbtbndlem1  48162  bgoldbtbndlem2  48163  bgoldbtbndlem3  48164  bgoldbtbnd  48166  dfnbgr6  48214  isuspgrimlem  48252  uhgrimisgrgric  48288  clnbgrgrim  48291  usgrgrtrirex  48307  isubgr3stgrlem4  48326  grilcbri2  48368  grlicsym  48370  grlictr  48372  gricgrlic  48375  gpgvtxedg0  48420  gpgvtxedg1  48421  gpgedg2ov  48423  gpgedg2iv  48424  pgnioedg1  48465  pgnioedg2  48466  pgnioedg3  48467  pgnioedg4  48468  pgnioedg5  48469  pgnbgreunbgrlem2lem3  48473  pgnbgreunbgrlem3  48475  pgnbgreunbgrlem5lem1  48477  pgnbgreunbgrlem5lem2  48478  pgnbgreunbgrlem5lem3  48479  pgnbgreunbgrlem6  48481  upgrwlkupwlk  48497  uspgrsprf1  48504  lmod0rng  48586  lidldomn1  48588  rngccatidALTV  48629  rngcinvALTV  48633  rhmsubcALTVlem4  48641  funcringcsetcALTV2lem9  48655  ringccatidALTV  48663  ringcbasbasALTV  48669  ztprmneprm  48704  pgrpgt2nabl  48723  lmodvsmdi  48736  ply1mulgsumlem2  48744  lincsumcl  48788  ellcoellss  48792  linindslinci  48805  islinindfis  48806  lincext3  48813  lindslinindimp2lem4  48818  lindslinindsimp2lem5  48819  lindslinindsimp2  48820  lindsrng01  48825  ldepspr  48830  lincresunit3lem1  48836  elfzolborelfzop1  48876  dignn0ldlem  48959  nn0sumshdiglem1  48978  1arymaptf1  48999  2arymaptf1  49010  rrx2xpref1o  49075  rrx2plord2  49079  rrx2plordisom  49080  line2ylem  49108  line2xlem  49110  line2y  49112  itschlc0xyqsol1  49123  inlinecirc02plem  49143  fullthinc  49806  tfis2d  50036  onsetrec  50064