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  2321  cbv1v  2340  exsb  2363  cbv1  2406  ax12b  2428  axc11n  2430  dvelimdf  2453  equvel  2460  dfsb1  2485  sbied  2507  dfmoeu  2535  mo3  2564  mo4  2566  2mo  2648  2eu6  2657  exists2  2662  pm2.61dne  3018  rexlimdv  3136  r19.21v  3162  r19.12  3286  2gencl  3472  3gencl  3473  vtocl2ga  3521  vtocl2gaf  3522  vtocl3gaf  3524  vtocl3ga  3526  vtocl4ga  3529  rspccv  3561  ceqex  3594  mob  3663  euind  3670  reuind  3699  2reu1  3835  sseq2  3948  nelss  3987  rexdifi  4090  reupick2  4271  disjeq0  4396  uneqdifeq  4432  sspw  4552  ssprsseq  4768  preq12b  4793  prnebg  4799  prel12g  4807  3elpr2eq  4849  iinss2  5000  trintss  5211  dtruALT2  5312  reusv2lem1  5340  alxfr  5349  ralxfrALT  5357  exexneq  5387  copsexgw  5443  copsexgwOLD  5444  copsexg  5445  snopeqop  5460  propeqop  5461  opthhausdorff  5471  opthhausdorff0  5472  pofun  5557  solin  5566  frss  5595  2optocl  5727  3optocl  5728  ssrel  5739  ssrel2  5741  ssrelrel  5752  relop  5805  dfres3  5949  asymref2  6080  xpidtr  6085  trin2  6086  poltletr  6095  imadifssran  6115  xp11  6139  relcnvtrg  6231  reuop  6257  tz7.7  6349  ordtr2  6368  suc11  6432  fundif  6547  fss  6684  f0dom0  6724  fv3  6858  tz6.12i  6866  mpteqb  6967  fveqdmss  7030  eldmrexrnb  7044  funopsnOLD  7102  funsndifnop  7105  tpres  7156  funfvima  7185  fvclss  7196  f1veqaeq  7211  fvf1pr  7262  isoselem  7296  oprabv  7427  ovg  7532  elovmpt3rab1  7627  sorpsscmpl  7688  iunpw  7725  trom  7826  limom  7833  peano5  7844  focdmex  7909  funelss  8000  funeldmdif  8001  bropopvvv  8040  bropfvvvvlem  8041  f1o2ndf1  8072  poxp  8078  soxp  8079  poxp2  8093  frxp2  8094  frxp3  8101  suppimacnv  8124  ressuppss  8133  ressuppssdif  8135  tposfn2  8198  wfr3g  8269  onnseq  8284  smoel  8300  smogt  8307  smoiso2  8309  tfr3  8338  tz7.48-2  8381  tz7.48-3  8383  tz7.49  8384  oecl  8472  oaordex  8493  oalimcl  8495  oaass  8496  omordi  8501  omlimcl  8513  odi  8514  omeulem1  8517  oen0  8522  nnawordi  8557  nnaass  8558  nnmordi  8567  omabs  8587  omsmolem  8593  naddssim  8621  brinxper  8673  iiner  8736  2ecoptocl  8755  3ecoptocl  8756  undifixp  8882  xpdom2  9010  xpf1o  9077  infensuc  9093  findcard2  9099  php  9141  isinf  9175  unblem2  9203  fodomfir  9238  infssuni  9256  finsschain  9269  fsuppunfi  9301  fsuppunbi  9302  marypha1  9347  hartogs  9459  card2on  9469  card2inf  9470  xpwdomg  9500  elirrv  9512  elirrvOLD  9513  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  11309  lemul1a  12009  squeeze0  12059  peano5nni  12177  nnadddir  12233  nnunb  12433  nn0lt2  12592  nn0le2is012  12593  fzind  12627  nn0ind-raph  12629  zindd  12630  uzin  12824  nn01to3  12891  xnn0xadd0  13199  xmulasslem  13237  icoshft  13426  fzen  13495  uzsubsubfz  13500  elfz0ubfz0  13586  elfz0fzfz0  13587  fz0fzelfz0  13588  elfzmlbp  13593  elfzodifsumelfzo  13686  ssfzo12bi  13716  fzoopth  13717  elfzonelfzo  13724  elfznelfzo  13728  injresinjlem  13745  injresinj  13746  modfzo0difsn  13905  modsumfzodifsn  13906  addmodlteq  13908  ssnn0fi  13947  fsuppmapnn0fiub0  13955  expcllem  14034  expeq0  14054  mulexp  14063  leexp2r  14136  bernneq  14191  facdiv  14249  hasheqf1oi  14313  hashnn0n0nn  14353  hashss  14371  hashgt12el  14384  hashgt12el2  14385  hashimarni  14403  hashle2pr  14439  pr2pwpr  14441  hashge2el2dif  14442  hashge2el2difr  14443  hashtpg  14447  hashge3el3dif  14449  exprelprel  14452  hash1to3  14454  hash3tpde  14455  tpfo  14462  fundmge2nop0  14464  fi1uzind  14469  ccatsymb  14545  swrdnd  14617  swrdnd2  14618  swrdnnn0nd  14619  swrdnd0  14620  pfxnd0  14651  swrdswrdlem  14666  swrdswrd  14667  pfxccatin12lem2a  14689  pfxccatin12lem1  14690  swrdccatin2  14691  pfxccatin12lem2  14693  pfxccatin12lem3  14694  pfxccat3  14696  swrdccat  14697  swrdccat3blem  14701  repsdf2  14740  repswswrd  14746  cshwidxmod  14765  cshwidx0  14768  cshf1  14772  cshweqrep  14783  cshw1  14784  2cshwcshw  14787  scshwfzeqfzo  14788  cshwcsh2id  14790  wwlktovfo  14920  relexpaddg  15015  iseraltlem2  15645  modfsummods  15756  clim2prod  15853  prodfn0  15859  prodfrec  15860  prodmo  15901  fprodabs  15939  binomfallfac  16006  fprodefsum  16060  dvdsaddre2b  16276  addmodlteqALT  16294  oddge22np1  16318  nn0enne  16346  nn0o1gt2  16350  sumeven  16356  sumodd  16357  dvdslegcd  16473  gcdneg  16491  dfgcd2  16515  rplpwr  16527  lcmf  16602  lcmftp  16605  lcmfunsnlem2lem1  16607  lcmfunsnlem2  16609  lcmfdvdsb  16612  coprmdvds1  16621  qredeq  16626  coprmprod  16630  coprmproddvdslem  16631  cncongr1  16636  cncongr2  16637  prm2orodd  16660  2mulprm  16662  nnnn0modprm0  16777  prm23lt5  16785  prm23ge5  16786  dvdsprmpweqnn  16856  dvdsprmpweqle  16857  oddprmdvds  16874  prmpwdvds  16875  prmreclem4  16890  ramcl  17000  prmgaplem6  17027  prmgaplem7  17028  prmgaplem8  17029  cshwshashlem1  17066  cshwshashlem2  17067  cshwshashlem3  17068  cshwrepswhash1  17073  setsn0fun  17143  setsstruct2  17144  imasleval  17505  mreiincl  17558  mreexexd  17614  inveq  17741  cicsym  17771  cictr  17772  initoid  17968  termoid  17969  initoeu2lem0  17980  initoeu2lem1  17981  initoeu2lem2  17982  initoeu2  17983  fthestrcsetc  18116  fthsetcestrc  18131  drsdirfi  18271  isnmgm  18612  mgmhmlin  18667  issubmgm2  18671  sgrpass  18693  insubm  18786  mgm2nsgrplem3  18891  dfgrp3lem  19014  cyccom  19178  symg2bas  19368  symgfix2  19391  symgextf1  19396  gsmsymgrfix  19403  pmtrprfv3  19429  psgnunilem4  19472  efgi2  19700  0ringnnzr  20502  rnghmsscmap  20607  rnghmsubcsetclem2  20609  rngcinv  20614  funcrngcsetc  20617  funcrngcsetcALT  20618  rhmsscmap  20636  rhmsubcsetclem2  20638  rhmsubcrngclem2  20644  ringcbasbas  20650  funcringcsetc  20651  rhmsubclem4  20665  rngqiprngimfo  21299  psgndiflemB  21580  psgndiflemA  21581  elfrlmbasn0  21743  lmictra  21825  mpfrcl  22063  gsummoncoe1  22273  mamufacex  22361  matecl  22390  dmatelnd  22461  dmatscmcl  22468  scmateALT  22477  scmatsgrp1  22487  scmatf1  22496  mavmulsolcl  22516  cramerimplem1  22648  cramerimplem2  22649  pmatcollpw3fi1  22753  mp2pm2mplem4  22774  pm2mpfo  22779  chmaidscmat  22813  fvmptnn04ifb  22816  chfacfscmul0  22823  chfacfpmmul0  22827  cayhamlem1  22831  cayhamlem3  22852  cayleyhamilton1  22857  fiinopn  22866  tgcl  22934  distop  22960  isclo2  23053  iscldtop  23060  ssnei2  23081  opnnei  23085  pnfnei  23185  mnfnei  23186  tgcnp  23218  cnpnei  23229  1stcelcls  23426  txcnpi  23573  cnmptcom  23643  fbfinnfr  23806  isfildlem  23822  snfil  23829  fbunfip  23834  fgcl  23843  elfm2  23913  fmco  23926  fbflim2  23942  cnpflf2  23965  flimfcls  23991  tmdgsum  24060  neibl  24466  tngngpim  24624  fgcfil  25238  caubl  25275  volsuplem  25522  ellimc3  25846  dvnadd  25896  dvnres  25898  cpnord  25902  dvnfre  25919  ply1divex  26102  cxpmul2  26653  fsumdvdsmul  27158  zabsle1  27259  gausslemma2dlem1a  27328  gausslemma2dlem3  27331  lgsquad2lem2  27348  2lgs  27370  2sq2  27396  2sqnn0  27401  2sqnn  27402  2sqreultlem  27410  2sqreunnltlem  27413  qabvexp  27589  ltsval2  27620  nolt02o  27659  sltsun1  27780  cutsun12  27782  madebday  27892  mulsprop  28122  precsexlem8  28206  precsexlem9  28207  noseqind  28284  om2noseqrdg  28296  n0cutlt  28351  peano5uzs  28396  expadds  28427  bdaypw2n0bndlem  28455  bdaypw2n0bnd  28456  axcontlem4  29036  umgredgprv  29176  umgrnloop  29177  upgrpredgv  29208  upgredgpr  29211  edglnl  29212  usgredgprvALT  29264  usgrnloopALT  29272  usgredg2v  29296  fusgrfis  29399  nbuhgr2vtx1edgblem  29420  nb3grprlem1  29449  cusgrsize2inds  29522  cusgrfi  29527  fusgrn0degnn0  29568  uspgrloopvtxel  29585  vtxdginducedm1lem4  29611  uhgr0edg0rgrb  29643  wlkl1loop  29706  wlk1walk  29707  upgriswlk  29709  upgrwlkvtxedg  29713  uspgr2wlkeq  29714  wlkv0  29718  wlksoneq1eq2  29731  wlkon2n0  29733  wlkreslem  29736  wlkres  29737  lfgrwlkprop  29754  pthdivtx  29795  2pthnloop  29799  spthonepeq  29820  uhgrwkspthlem2  29822  uhgrwkspth  29823  usgr2wlkneq  29824  usgr2trlncl  29828  usgr2pthlem  29831  usgr2pth  29832  cyclnspth  29869  lfgrn1cycl  29873  usgr2trlncrct  29874  uspgrn2crct  29876  crctcshwlkn0lem3  29880  crctcshwlkn0lem5  29882  wwlknp  29911  wspthneq1eq2  29928  0enwwlksnge1  29932  wlklnwwlkln1  29936  wlkiswwlks2  29943  wlkiswwlksupgr2  29945  wlklnwwlkln2lem  29950  wwlksnred  29960  wwlksnextbi  29962  wwlksnredwwlkn0  29964  wwlksnextwrd  29965  wwlksnextinj  29967  wwlksnextproplem3  29979  wwlksnextprop  29980  wspthsnwspthsnon  29984  wspthsnonn0vne  29985  2pthon3v  30011  umgr2adedgwlkonALT  30015  umgr2wlk  30017  umgr2wlkon  30018  usgrwwlks2on  30026  umgrwwlks2on  30027  elwspths2on  30030  elwspths2onw  30031  usgr2wspthons3  30035  elwwlks2  30037  rusgrnumwwlk  30046  clwwlkccatlem  30059  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  clwlkclwwlkf1lem3  30076  erclwwlkeqlen  30089  clwwlknwwlksn  30108  loopclwwlkn1b  30112  clwwlkf1  30119  wwlksext2clwwlk  30127  eleclclwwlknlem2  30131  umgr2cwwk2dif  30134  eleclclwwlkn  30146  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  clwwlknonwwlknonb  30176  clwwlknonex2lem2  30178  clwwlknonex2  30179  1pthon2v  30223  upgr3v3e3cycl  30250  uhgr3cyclexlem  30251  uhgr3cyclex  30252  eupth2lem3lem4  30301  frgr3vlem1  30343  frgr3vlem2  30344  3vfriswmgrlem  30347  3vfriswmgr  30348  3cyclfrgrrn1  30355  n4cyclfrgr  30361  frgrncvvdeqlem3  30371  frgrncvvdeqlem6  30374  frgrncvvdeqlem7  30375  frgrncvvdeqlem8  30376  frgrwopreglem4a  30380  frgrwopreglem3  30384  frgrwopreg1  30388  frgrwopreg2  30389  frgrwopreglem5lem  30390  frgrwopreglem5ALT  30392  frgrwopreg  30393  fusgr2wsp2nb  30404  2wspmdisj  30407  numclwwlk1lem2foa  30424  numclwwlk1lem2f1  30427  numclwwlk1lem2fo  30428  numclwwlk1  30431  wlkl0  30437  numclwwlk2lem1  30446  numclwlk2lem2f  30447  numclwlk2lem2f1o  30449  frgrreg  30464  frgrregord013  30465  frgrregord13  30466  friendshipgt3  30468  friendship  30469  eulplig  30556  ipassi  30912  ubthlem2  30942  isch3  31312  shintcli  31400  shmodsi  31460  spansncvi  31723  hoaddsub  31887  eigorthi  31908  pjss2coi  32235  pjnormssi  32239  pj3cor1i  32280  strb  32329  dmdmd  32371  mdsl0  32381  csmdsymi  32405  chrelat2i  32436  mdsymlem3  32476  mdsymlem6  32479  sumdmdlem2  32490  opreu2reuALT  32546  ssrelf  32688  gsumwun  33137  r1filim  35247  trssfir1om  35255  fineqvinfep  35269  trssfir1omregs  35280  onvf1odlem4  35288  spthcycl  35311  loop1cycl  35319  cvmlift2lem1  35484  satfrel  35549  satfrnmapom  35552  fmlafvel  35567  fmla1  35569  gonarlem  35576  gonar  35577  goalrlem  35578  goalr  35579  satffunlem  35583  satffunlem1lem1  35584  satffunlem2lem1  35586  satffun  35591  satefvfmla1  35607  mrsubvrs  35704  mclsax  35751  3ccased  35901  dfon2lem3  35965  rdgprc  35974  cgrextend  36190  btwndiff  36209  btwnconn1lem12  36280  brsegle  36290  broutsideof2  36304  funray  36322  in-ax8  36406  ss-ax8  36407  elicc3  36499  nn0prpwlem  36504  nn0prpw  36505  fnessref  36539  neibastop2lem  36542  filnetlem4  36563  meran1  36593  waj-ax  36596  arg-ax  36598  axtco1from2  36657  dfttc4  36712  mh-inf3f1  36723  mh-regprimbi  36727  bj-nnclavc  36808  bj-con2com  36825  bj-axdd2  36857  bj-alrimg  36878  bj-exlimg  36900  bj-exalimi  36910  bj-eximcom  36911  bj-ssbid1ALT  36959  bj-sb  36984  bj-snsetex  37270  bj-axseprep  37381  bj-axreprepsep  37382  bj-restpw  37404  bj-finsumval0  37599  mptsnunlem  37654  icoreclin  37673  relowlpssretop  37680  inunissunidif  37691  rdgssun  37694  finorwe  37698  domalom  37720  wl-dral1d  37856  wl-exeq  37859  wl-lem-exsb  37891  wl-eujustlem1  37913  poimirlem29  37970  poimirlem32  37973  fdc  38066  seqpo  38068  incsequz  38069  isismty  38122  ismtybndlem  38127  heibor1lem  38130  ismgmOLD  38171  isexid2  38176  ghomco  38212  pridlc  38392  relcnveq3  38648  elrelscnveq3  38948  cdleme18d  40741  tendovalco  41211  cdlemn11pre  41656  dihord2pre  41671  indstrd  42632  unitscyglem3  42636  eu6w  43109  incssnn0  43143  fphpd  43244  jm2.19lem3  43419  setindtr  43452  islssfg2  43499  mpaaeu  43578  ordnexbtwnsuc  43695  oaabsb  43722  succlg  43756  oacl2g  43758  omabs2  43760  omcl2  43761  omcl3g  43762  pr2cv  43975  refimssco  44034  iunrelexpmin1  44135  iunrelexpmin2  44139  trclimalb2  44153  clsk1indlem3  44470  tfindsd  44637  mnurndlem1  44708  nzss  44744  sb5ALT  44952  truniALT  44968  ee223  45061  3orbi123VD  45276  sbc3orgVD  45277  exbirVD  45279  exbiriVD  45280  sbcim2gVD  45301  trsbcVD  45303  truniALTVD  45304  onfrALTlem3VD  45313  onfrALTlem2VD  45315  csbrngVD  45322  19.41rgVD  45328  ax6e2eqVD  45333  ax6e2ndeqVD  45335  2uasbanhVD  45337  sb5ALTVD  45339  vk15.4jVD  45340  infxrunb3rnmpt  45856  stoweidlem26  46454  et-equeucl  47300  hirstL-ax3  47340  rexsb  47547  rexrsb  47548  euoreqb  47557  2reu8i  47561  afvres  47620  tz6.12-afv  47621  afvco2  47624  afv2orxorb  47676  afv2res  47687  tz6.12-afv2  47688  tz6.12i-afv2  47691  dfatcolem  47703  zm1nn  47750  2ffzoeq  47776  smonoord  47825  iccpartiltu  47882  iccpartlt  47884  iccpartltu  47885  iccpartgtl  47886  iccpartgt  47887  iccpartleu  47888  iccpartgel  47889  icceuelpart  47896  iccpartnel  47898  lswn0  47904  ichnreuop  47932  ichreuopeq  47933  prsprel  47947  sprsymrelfvlem  47950  sprsymrelf1lem  47951  sprsymrelfolem2  47953  prproropf1olem4  47966  paireqne  47971  prprelb  47976  reupr  47982  goldbachth  48010  odz2prm2pw  48026  fmtno4prmfac  48035  fmtno4prmfac193  48036  prmdvdsfmtnof1lem2  48048  2pwp1prmfmtno  48053  lighneallem2  48069  lighneallem4b  48072  lighneallem4  48073  requad2  48099  odd2prm2  48194  mogoldbblem  48196  gbepos  48234  gbowgt5  48238  gbowge7  48239  stgoldbwt  48252  sbgoldbwt  48253  sbgoldbst  48254  sbgoldbaltlem1  48255  sbgoldbalt  48257  sbgoldbo  48263  nnsum3primesle9  48270  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  bgoldbtbndlem1  48281  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  bgoldbtbnd  48285  dfnbgr6  48333  isuspgrimlem  48371  uhgrimisgrgric  48407  clnbgrgrim  48410  usgrgrtrirex  48426  isubgr3stgrlem4  48445  grilcbri2  48487  grlicsym  48489  grlictr  48491  gricgrlic  48494  gpgvtxedg0  48539  gpgvtxedg1  48540  gpgedg2ov  48542  gpgedg2iv  48543  pgnioedg1  48584  pgnioedg2  48585  pgnioedg3  48586  pgnioedg4  48587  pgnioedg5  48588  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem5lem1  48596  pgnbgreunbgrlem5lem2  48597  pgnbgreunbgrlem5lem3  48598  pgnbgreunbgrlem6  48600  upgrwlkupwlk  48616  uspgrsprf1  48623  lmod0rng  48705  lidldomn1  48707  rngccatidALTV  48748  rngcinvALTV  48752  rhmsubcALTVlem4  48760  funcringcsetcALTV2lem9  48774  ringccatidALTV  48782  ringcbasbasALTV  48788  ztprmneprm  48823  pgrpgt2nabl  48842  lmodvsmdi  48855  ply1mulgsumlem2  48863  lincsumcl  48907  ellcoellss  48911  linindslinci  48924  islinindfis  48925  lincext3  48932  lindslinindimp2lem4  48937  lindslinindsimp2lem5  48938  lindslinindsimp2  48939  lindsrng01  48944  ldepspr  48949  lincresunit3lem1  48955  elfzolborelfzop1  48995  dignn0ldlem  49078  nn0sumshdiglem1  49097  1arymaptf1  49118  2arymaptf1  49129  rrx2xpref1o  49194  rrx2plord2  49198  rrx2plordisom  49199  line2ylem  49227  line2xlem  49229  line2y  49231  itschlc0xyqsol1  49242  inlinecirc02plem  49262  fullthinc  49925  tfis2d  50155  onsetrec  50183