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  exptOLD  178  jad  188  pm2.61  193  syl5ibcom  247  syl5ibrcom  249  pm5.501  368  impcom  411  impd  414  expcom  417  expdcom  418  simplbi2com  506  imdistanri  577  syldbl2  852  jaod  870  orel1  899  pm2.62  910  pm2.75  944  pm2.64  954  ccased  1049  dedlem0b  1055  3impd  1361  3expd  1366  mp3an1i  1474  minimp  1640  meredith  1660  19.35  1896  speimfw  1982  equtrr  2041  equeucl  2043  ax12ev2  2214  sbiedw  2347  cbv1v  2366  exsb  2389  cbv1  2432  ax12b  2454  axc11n  2456  dvelimdf  2479  equvel  2486  dfsb1  2511  sbied  2533  dfmoeu  2561  mo3  2590  mo4  2592  2mo  2674  2eu6  2682  exists2  2687  pm2.61dne  3042  rexlimdv  3160  r19.21v  3186  r19.12  3310  2gencl  3495  3gencl  3496  vtocl2ga  3542  vtocl2gaf  3543  vtocl3gaf  3544  vtocl3ga  3545  vtocl4ga  3547  rspccv  3578  ceqex  3611  mob  3679  euind  3686  reuind  3715  2reu1  3850  sseq2  3962  nelss  4002  rexdifi  4103  reupick2  4283  disjeq0  4409  uneqdifeq  4445  sspw  4565  ssprsseq  4782  preq12b  4807  prnebg  4813  prel12g  4821  3elpr2eq  4863  iinss2  5014  trintss  5225  dtruALT2  5326  reusv2lem1  5354  alxfr  5363  ralxfrALT  5371  exexneq  5401  copsexgw  5457  copsexgwOLD  5458  copsexg  5459  snopeqop  5474  propeqop  5475  opthhausdorff  5485  opthhausdorff0  5486  pofun  5571  solin  5580  frss  5609  2optocl  5741  3optocl  5742  ssrel  5753  ssrel2  5755  ssrelrel  5766  relop  5820  dfres3  5968  asymref2  6101  xpidtr  6106  trin2  6107  poltletr  6116  imadifssran  6133  xp11  6157  relcnvtrg  6250  reuop  6276  tz7.7  6368  ordtr2  6387  suc11  6451  fundif  6566  fss  6704  f0dom0  6744  fv3  6881  tz6.12i  6889  mpteqb  6991  fveqdmss  7055  eldmrexrnb  7069  funopsnOLD  7127  funsndifnop  7130  tpres  7181  funfvima  7210  fvclss  7221  f1veqaeq  7236  fvf1pr  7287  isoselem  7321  oprabv  7452  ovg  7557  elovmpt3rab1  7652  sorpsscmpl  7713  iunpw  7750  trom  7851  limom  7858  peano5  7870  focdmex  7933  funelss  8024  funeldmdif  8025  bropopvvv  8064  bropfvvvvlem  8065  f1o2ndf1  8096  poxp  8103  soxp  8104  poxp2  8118  frxp2  8119  frxp3  8126  suppimacnv  8149  ressuppss  8158  ressuppssdif  8160  tposfn2  8223  wfr3g  8295  onnseq  8310  smoel  8326  smogt  8333  smoiso2  8335  tfr3  8365  tz7.48-2  8408  tz7.48-3  8410  tz7.49  8411  oecl  8501  oaordex  8522  oalimcl  8524  oaass  8525  omordi  8530  omlimcl  8542  odi  8543  omeulem1  8546  oen0  8551  nnawordi  8586  nnaass  8587  nnmordi  8596  omabs  8616  omsmolem  8622  naddssim  8651  brinxper  8703  iiner  8766  2ecoptocl  8785  3ecoptocl  8786  undifixp  8912  xpdom2  9040  xpf1o  9107  infensuc  9123  findcard2  9129  php  9171  isinf  9205  unblem2  9233  fodomfir  9268  infssuni  9286  finsschain  9299  fsuppunfi  9331  fsuppunbi  9332  marypha1  9377  hartogs  9489  card2on  9499  card2inf  9500  xpwdomg  9530  elirrvOLD  9543  elirrvOLDOLD  9544  en3lp  9566  preleqg  9567  inf3lem1  9580  inf3lem2  9581  inf3lem3  9582  inf3lem5  9584  noinfep  9612  ttrclss  9672  ttrclselem2  9678  trcl  9680  tcel  9695  frr3g  9711  rankonidlem  9783  scottex  9840  djuunxp  9876  eldju2ndl  9879  updjud  9889  dif1card  9963  fodomnum  10010  cardaleph  10042  kmlem9  10112  kmlem13  10116  cflim2  10217  cfsmolem  10224  infpssrlem3  10259  isfin7-2  10350  fin1a2lem6  10359  fin1a2lem12  10365  domtriomlem  10396  axdc3lem4  10407  axdc4lem  10409  zorn2lem3  10452  zorn2lem4  10453  zorn2lem5  10454  zorn2lem7  10456  zornn0g  10459  axdclem2  10474  ondomon  10517  alephval2  10527  cfpwsdom  10539  wuncval2  10702  grupr  10752  gruiun  10754  ingru  10770  grothomex  10784  indpi  10862  nqereu  10884  prlem934  10988  reclem2pr  11003  mulgt0sr  11060  supsrlem  11066  1re  11178  dedekind  11343  lemul1a  12042  squeeze0  12092  peano5nni  12210  nnadddir  12266  nnunb  12474  nn0lt2  12633  nn0le2is012  12634  fzind  12668  nn0ind-raph  12670  zindd  12671  uzin  12872  nn01to3  12939  xnn0xadd0  13247  xmulasslem  13285  icoshft  13474  fzen  13543  uzsubsubfz  13548  elfz0ubfz0  13634  elfz0fzfz0  13635  fz0fzelfz0  13636  elfzmlbp  13641  elfzodifsumelfzo  13734  ssfzo12bi  13764  fzoopth  13765  elfzonelfzo  13772  elfznelfzo  13776  injresinjlem  13793  injresinj  13794  modfzo0difsn  13953  modsumfzodifsn  13954  addmodlteq  13956  ssnn0fi  13995  fsuppmapnn0fiub0  14003  expcllem  14082  expeq0  14102  mulexp  14111  leexp2r  14184  bernneq  14239  facdiv  14297  hasheqf1oi  14361  hashnn0n0nn  14401  hashss  14419  hashgt12el  14432  hashgt12el2  14433  hashimarni  14451  hashle2pr  14487  pr2pwpr  14489  hashge2el2dif  14490  hashge2el2difr  14491  hashtpg  14495  hashge3el3dif  14497  exprelprel  14500  hash1to3  14502  hash3tpde  14503  tpfo  14510  fundmge2nop0  14512  fi1uzind  14517  ccatsymb  14593  swrdnd  14665  swrdnd2  14666  swrdnnn0nd  14667  swrdnd0  14668  pfxnd0  14699  swrdswrdlem  14714  swrdswrd  14715  pfxccatin12lem2a  14737  pfxccatin12lem1  14738  swrdccatin2  14739  pfxccatin12lem2  14741  pfxccatin12lem3  14742  pfxccat3  14744  swrdccat  14745  swrdccat3blem  14749  repsdf2  14788  repswswrd  14794  cshwidxmod  14813  cshwidx0  14816  cshf1  14820  cshweqrep  14831  cshw1  14832  2cshwcshw  14835  scshwfzeqfzo  14836  cshwcsh2id  14838  wwlktovfo  14968  relexpaddg  15063  iseraltlem2  15693  modfsummods  15804  clim2prod  15901  prodfn0  15907  prodfrec  15908  prodmo  15949  fprodabs  15987  binomfallfac  16054  fprodefsum  16108  dvdsaddre2b  16324  addmodlteqALT  16342  oddge22np1  16366  nn0enne  16394  nn0o1gt2  16398  sumeven  16404  sumodd  16405  dvdslegcd  16521  gcdneg  16539  dfgcd2  16563  rplpwr  16575  lcmf  16650  lcmftp  16653  lcmfunsnlem2lem1  16655  lcmfunsnlem2  16657  lcmfdvdsb  16660  coprmdvds1  16669  qredeq  16674  coprmprod  16678  coprmproddvdslem  16679  cncongr1  16684  cncongr2  16685  prm2orodd  16708  2mulprm  16710  nnnn0modprm0  16825  prm23lt5  16833  prm23ge5  16834  dvdsprmpweqnn  16904  dvdsprmpweqle  16905  oddprmdvds  16922  prmpwdvds  16923  prmreclem4  16938  ramcl  17048  prmgaplem6  17075  prmgaplem7  17076  prmgaplem8  17077  cshwshashlem1  17114  cshwshashlem2  17115  cshwshashlem3  17116  cshwrepswhash1  17121  setsn0fun  17192  setsstruct2  17193  imasleval  17554  mreiincl  17607  mreexexd  17663  inveq  17790  cicsym  17820  cictr  17821  initoid  18017  termoid  18018  initoeu2lem0  18029  initoeu2lem1  18030  initoeu2lem2  18031  initoeu2  18032  fthestrcsetc  18165  fthsetcestrc  18180  drsdirfi  18320  isnmgm  18661  mgmhmlin  18716  issubmgm2  18720  sgrpass  18742  insubm  18835  mgm2nsgrplem3  18940  dfgrp3lem  19063  cyccom  19227  symg2bas  19416  symgfix2  19439  symgextf1  19444  gsmsymgrfix  19451  pmtrprfv3  19477  psgnunilem4  19520  efgi2  19748  0ringnnzr  20554  rnghmsscmap  20659  rnghmsubcsetclem2  20661  rngcinv  20666  funcrngcsetc  20669  funcrngcsetcALT  20670  rhmsscmap  20688  rhmsubcsetclem2  20690  rhmsubcrngclem2  20696  ringcbasbas  20702  funcringcsetc  20703  rhmsubclem4  20717  rngqiprngimfo  21351  psgndiflemB  21632  psgndiflemA  21633  elfrlmbasn0  21795  lmictra  21877  mpfrcl  22118  gsummoncoe1  22351  mamufacex  22436  matecl  22465  dmatelnd  22536  dmatscmcl  22543  scmateALT  22552  scmatsgrp1  22562  scmatf1  22571  mavmulsolcl  22591  cramerimplem1  22723  cramerimplem2  22724  pmatcollpw3fi1  22828  mp2pm2mplem4  22849  pm2mpfo  22854  chmaidscmat  22888  fvmptnn04ifb  22891  chfacfscmul0  22898  chfacfpmmul0  22902  cayhamlem1  22906  cayhamlem3  22927  cayleyhamilton1  22932  fiinopn  22941  tgcl  23009  distop  23035  isclo2  23128  iscldtop  23135  ssnei2  23156  opnnei  23160  pnfnei  23260  mnfnei  23261  tgcnp  23293  cnpnei  23304  1stcelcls  23501  txcnpi  23648  cnmptcom  23718  fbfinnfr  23881  isfildlem  23897  snfil  23904  fbunfip  23909  fgcl  23918  elfm2  23988  fmco  24001  fbflim2  24017  cnpflf2  24040  flimfcls  24066  tmdgsum  24135  neibl  24541  tngngpim  24699  fgcfil  25313  caubl  25350  volsuplem  25597  ellimc3  25921  dvnadd  25971  dvnres  25973  cpnord  25977  dvnfre  25994  ply1divex  26177  cxpmul2  26731  fsumdvdsmul  27236  zabsle1  27337  gausslemma2dlem1a  27406  gausslemma2dlem3  27409  lgsquad2lem2  27426  2lgs  27448  2sq2  27474  2sqnn0  27479  2sqnn  27480  2sqreultlem  27488  2sqreunnltlem  27491  qabvexp  27667  ltsval2  27697  nolt02o  27736  sltsun1  27858  cutsun12  27860  madebday  27970  mulsprop  28200  precsexlem8  28284  precsexlem9  28285  noseqind  28362  om2noseqrdg  28374  n0cutlt  28429  peano5uzs  28474  expadds  28505  bdaypw2n0bndlem  28533  bdaypw2n0bnd  28534  axcontlem4  29114  umgredgprv  29254  umgrnloop  29255  upgrpredgv  29286  upgredgpr  29289  edglnl  29290  usgredgprvALT  29342  usgrnloopALT  29350  usgredg2v  29374  fusgrfis  29477  nbuhgr2vtx1edgblem  29498  nb3grprlem1  29527  cusgrsize2inds  29600  cusgrfi  29605  fusgrn0degnn0  29646  uspgrloopvtxel  29663  vtxdginducedm1lem4  29689  uhgr0edg0rgrb  29721  wlkl1loop  29784  wlk1walk  29785  upgriswlk  29787  upgrwlkvtxedg  29791  uspgr2wlkeq  29792  wlkv0  29796  wlksoneq1eq2  29809  wlkon2n0  29811  wlkreslem  29814  wlkres  29815  lfgrwlkprop  29832  pthdivtx  29873  2pthnloop  29877  spthonepeq  29898  uhgrwkspthlem2  29900  uhgrwkspth  29901  usgr2wlkneq  29902  usgr2trlncl  29906  usgr2pthlem  29909  usgr2pth  29910  cyclnspth  29947  lfgrn1cycl  29951  usgr2trlncrct  29952  uspgrn2crct  29954  crctcshwlkn0lem3  29958  crctcshwlkn0lem5  29960  wwlknp  29989  wspthneq1eq2  30006  0enwwlksnge1  30010  wlklnwwlkln1  30014  wlkiswwlks2  30021  wlkiswwlksupgr2  30023  wlklnwwlkln2lem  30028  wwlksnred  30038  wwlksnextbi  30040  wwlksnredwwlkn0  30042  wwlksnextwrd  30043  wwlksnextinj  30045  wwlksnextproplem3  30057  wwlksnextprop  30058  wspthsnwspthsnon  30062  wspthsnonn0vne  30063  2pthon3v  30089  umgr2adedgwlkonALT  30093  umgr2wlk  30095  umgr2wlkon  30096  usgrwwlks2on  30104  umgrwwlks2on  30105  elwspths2on  30108  elwspths2onw  30109  usgr2wspthons3  30113  elwwlks2  30115  rusgrnumwwlk  30124  clwwlkccatlem  30137  clwlkclwwlklem2a4  30145  clwlkclwwlklem2a  30146  clwlkclwwlklem2  30148  clwlkclwwlkf1lem3  30154  erclwwlkeqlen  30167  clwwlknwwlksn  30186  loopclwwlkn1b  30190  clwwlkf1  30197  wwlksext2clwwlk  30205  eleclclwwlknlem2  30209  umgr2cwwk2dif  30212  eleclclwwlkn  30224  hashecclwwlkn1  30225  umgrhashecclwwlk  30226  clwwlknonwwlknonb  30254  clwwlknonex2lem2  30256  clwwlknonex2  30257  1pthon2v  30301  upgr3v3e3cycl  30328  uhgr3cyclexlem  30329  uhgr3cyclex  30330  eupth2lem3lem4  30379  frgr3vlem1  30421  frgr3vlem2  30422  3vfriswmgrlem  30425  3vfriswmgr  30426  3cyclfrgrrn1  30433  n4cyclfrgr  30439  frgrncvvdeqlem3  30449  frgrncvvdeqlem6  30452  frgrncvvdeqlem7  30453  frgrncvvdeqlem8  30454  frgrwopreglem4a  30458  frgrwopreglem3  30462  frgrwopreg1  30466  frgrwopreg2  30467  frgrwopreglem5lem  30468  frgrwopreglem5ALT  30470  frgrwopreg  30471  fusgr2wsp2nb  30482  2wspmdisj  30485  numclwwlk1lem2foa  30502  numclwwlk1lem2f1  30505  numclwwlk1lem2fo  30506  numclwwlk1  30509  wlkl0  30515  numclwwlk2lem1  30524  numclwlk2lem2f  30525  numclwlk2lem2f1o  30527  frgrreg  30542  frgrregord013  30543  frgrregord13  30544  friendshipgt3  30546  friendship  30547  eulplig  30634  ipassi  30990  ubthlem2  31020  isch3  31390  shintcli  31478  shmodsi  31538  spansncvi  31801  hoaddsub  31965  eigorthi  31986  pjss2coi  32313  pjnormssi  32317  pj3cor1i  32358  strb  32407  dmdmd  32449  mdsl0  32459  csmdsymi  32483  chrelat2i  32514  mdsymlem3  32554  mdsymlem6  32557  sumdmdlem2  32568  opreu2reuALT  32624  ssrelf  32767  gsumwun  33217  r1filim  35364  trssfir1om  35371  fineqvinfep  35385  trssfir1omregs  35396  onvf1odlem4  35413  spthcycl  35443  loop1cycl  35451  cvmlift2lem1  35616  satfrel  35681  satfrnmapom  35684  fmlafvel  35699  fmla1  35701  gonarlem  35708  gonar  35709  goalrlem  35710  goalr  35711  satffunlem  35715  satffunlem1lem1  35716  satffunlem2lem1  35718  satffun  35723  satefvfmla1  35739  mrsubvrs  35836  mclsax  35883  3ccased  36033  dfon2lem3  36097  rdgprc  36106  cgrextend  36322  btwndiff  36341  btwnconn1lem12  36412  brsegle  36422  broutsideof2  36436  funray  36454  in-ax8  36548  ss-ax8  36549  elicc3  36641  nn0prpwlem  36646  nn0prpw  36647  fnessref  36681  neibastop2lem  36684  filnetlem4  36705  meran1  36735  waj-ax  36738  arg-ax  36740  axtco1from2  36799  dfttc4  36854  mh-inf3f1  36865  mh-regprimbi  36869  bj-nnclavc  36950  bj-con2com  36967  bj-axdd2  36999  bj-alrimg  37020  bj-exlimg  37042  bj-exalimi  37052  bj-eximcom  37053  bj-ssbid1ALT  37101  bj-sb  37126  bj-snsetex  37412  bj-axseprep  37523  bj-axreprepsep  37524  bj-restpw  37546  bj-finsumval0  37741  mptsnunlem  37796  icoreclin  37815  relowlpssretop  37822  inunissunidif  37833  rdgssun  37836  finorwe  37840  domalom  37862  wl-dral1d  37998  wl-exeq  38001  wl-lem-exsb  38033  wl-eujustlem1  38055  poimirlem29  38112  poimirlem32  38115  fdc  38208  seqpo  38210  incsequz  38211  isismty  38264  ismtybndlem  38269  heibor1lem  38272  ismgmOLD  38313  isexid2  38318  ghomco  38354  pridlc  38534  relcnveq3  38790  elrelscnveq3  39090  cdleme18d  40883  tendovalco  41353  cdlemn11pre  41798  dihord2pre  41813  indstrd  42774  unitscyglem3  42778  eu6w  43222  incssnn0  43256  fphpd  43357  jm2.19lem3  43532  setindtr  43565  islssfg2  43612  mpaaeu  43691  ordnexbtwnsuc  43808  oaabsb  43835  succlg  43869  oacl2g  43871  omabs2  43873  omcl2  43874  omcl3g  43875  pr2cv  44088  refimssco  44147  iunrelexpmin1  44248  iunrelexpmin2  44252  trclimalb2  44266  clsk1indlem3  44583  tfindsd  44750  mnurndlem1  44821  nzss  44857  sb5ALT  45065  truniALT  45081  ee223  45174  3orbi123VD  45389  sbc3orgVD  45390  exbirVD  45392  exbiriVD  45393  sbcim2gVD  45414  trsbcVD  45416  truniALTVD  45417  onfrALTlem3VD  45426  onfrALTlem2VD  45428  csbrngVD  45435  19.41rgVD  45441  ax6e2eqVD  45446  ax6e2ndeqVD  45448  2uasbanhVD  45450  sb5ALTVD  45452  vk15.4jVD  45453  infxrunb3rnmpt  45966  stoweidlem26  46564  et-equeucl  47410  hirstL-ax3  47450  rexsb  47657  rexrsb  47658  euoreqb  47667  2reu8i  47671  afvres  47730  tz6.12-afv  47731  afvco2  47734  afv2orxorb  47786  afv2res  47797  tz6.12-afv2  47798  tz6.12i-afv2  47801  dfatcolem  47813  zm1nn  47860  2ffzoeq  47886  smonoord  47935  iccpartiltu  47992  iccpartlt  47994  iccpartltu  47995  iccpartgtl  47996  iccpartgt  47997  iccpartleu  47998  iccpartgel  47999  icceuelpart  48006  iccpartnel  48008  lswn0  48014  ichnreuop  48042  ichreuopeq  48043  prsprel  48057  sprsymrelfvlem  48060  sprsymrelf1lem  48061  sprsymrelfolem2  48063  prproropf1olem4  48076  paireqne  48081  prprelb  48086  reupr  48092  goldbachth  48120  odz2prm2pw  48136  fmtno4prmfac  48145  fmtno4prmfac193  48146  prmdvdsfmtnof1lem2  48158  2pwp1prmfmtno  48163  lighneallem2  48179  lighneallem4b  48182  lighneallem4  48183  requad2  48209  odd2prm2  48304  mogoldbblem  48306  gbepos  48344  gbowgt5  48348  gbowge7  48349  stgoldbwt  48362  sbgoldbwt  48363  sbgoldbst  48364  sbgoldbaltlem1  48365  sbgoldbalt  48367  sbgoldbo  48373  nnsum3primesle9  48380  nnsum4primesodd  48382  nnsum4primesoddALTV  48383  nnsum4primeseven  48386  nnsum4primesevenALTV  48387  bgoldbtbndlem1  48391  bgoldbtbndlem2  48392  bgoldbtbndlem3  48393  bgoldbtbnd  48395  dfnbgr6  48443  isuspgrimlem  48481  uhgrimisgrgric  48517  clnbgrgrim  48520  usgrgrtrirex  48536  isubgr3stgrlem4  48555  grilcbri2  48597  grlicsym  48599  grlictr  48601  gricgrlic  48604  gpgvtxedg0  48649  gpgvtxedg1  48650  gpgedg2ov  48652  gpgedg2iv  48653  pgnioedg1  48694  pgnioedg2  48695  pgnioedg3  48696  pgnioedg4  48697  pgnioedg5  48698  pgnbgreunbgrlem2lem3  48702  pgnbgreunbgrlem3  48704  pgnbgreunbgrlem5lem1  48706  pgnbgreunbgrlem5lem2  48707  pgnbgreunbgrlem5lem3  48708  pgnbgreunbgrlem6  48710  upgrwlkupwlk  48726  uspgrsprf1  48733  lmod0rng  48815  lidldomn1  48817  rngccatidALTV  48858  rngcinvALTV  48862  rhmsubcALTVlem4  48870  funcringcsetcALTV2lem9  48884  ringccatidALTV  48892  ringcbasbasALTV  48898  ztprmneprm  48933  pgrpgt2nabl  48952  lmodvsmdi  48965  ply1mulgsumlem2  48973  lincsumcl  49017  ellcoellss  49021  linindslinci  49034  islinindfis  49035  lincext3  49042  lindslinindimp2lem4  49047  lindslinindsimp2lem5  49048  lindslinindsimp2  49049  lindsrng01  49054  ldepspr  49059  lincresunit3lem1  49065  elfzolborelfzop1  49105  dignn0ldlem  49188  nn0sumshdiglem1  49207  1arymaptf1  49228  2arymaptf1  49239  rrx2xpref1o  49304  rrx2plord2  49308  rrx2plordisom  49309  line2ylem  49337  line2xlem  49339  line2y  49341  itschlc0xyqsol1  49352  inlinecirc02plem  49372  fullthinc  50035  tfis2d  50265  onsetrec  50293