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  3132  r19.21v  3158  r19.12  3288  2gencl  3490  3gencl  3491  vtocl2ga  3544  vtocl2gaf  3545  vtocl3gaf  3547  vtocl3ga  3549  vtocl4ga  3552  rspccv  3585  ceqex  3618  mob  3688  euind  3695  reuind  3724  2reu1  3860  sseq2  3973  nelss  4012  rexdifi  4113  reupick2  4294  disjeq0  4419  uneqdifeq  4456  sspw  4574  ssprsseq  4789  preq12b  4814  prnebg  4820  prel12g  4828  3elpr2eq  4870  iinss2  5021  trintss  5233  dtruALT2  5325  reusv2lem1  5353  alxfr  5362  ralxfrALT  5370  exexneq  5394  dtruOLD  5401  copsexgw  5450  copsexg  5451  snopeqop  5466  propeqop  5467  opthhausdorff  5477  opthhausdorff0  5478  pofun  5564  solin  5573  frss  5602  2optocl  5734  3optocl  5735  ssrel  5745  ssrelOLD  5746  ssrel2  5748  ssrelrel  5759  relop  5814  dfres3  5955  asymref2  6090  xpidtr  6095  trin2  6096  poltletr  6105  imadifssran  6124  xp11  6148  relcnvtrg  6239  reuop  6266  tz7.7  6358  ordtr2  6377  suc11  6441  iotavalOLD  6485  funmoOLD  6532  fundif  6565  fss  6704  f0dom0  6744  fv3  6876  tz6.12i  6886  mpteqb  6987  fveqdmss  7050  eldmrexrnb  7064  funopsn  7120  funsndifnop  7123  tpres  7175  funfvima  7204  fvclss  7215  f1veqaeq  7231  fvf1pr  7282  isoselem  7316  oprabv  7449  ovg  7554  elovmpt3rab1  7649  sorpsscmpl  7710  iunpw  7747  trom  7851  limom  7858  peano5  7869  focdmex  7934  funelss  8026  funeldmdif  8027  bropopvvv  8069  bropfvvvvlem  8070  f1o2ndf1  8101  poxp  8107  soxp  8108  poxp2  8122  frxp2  8123  frxp3  8130  suppimacnv  8153  ressuppss  8162  ressuppssdif  8164  tposfn2  8227  wfr3g  8298  onnseq  8313  smoel  8329  smogt  8336  smoiso2  8338  tfr3  8367  tz7.48-2  8410  tz7.48-3  8412  tz7.49  8413  oecl  8501  oaordex  8522  oalimcl  8524  oaass  8525  omordi  8530  omlimcl  8542  odi  8543  omeulem1  8546  oen0  8550  nnawordi  8585  nnaass  8586  nnmordi  8595  omabs  8615  omsmolem  8621  naddssim  8649  brinxper  8700  iiner  8762  2ecoptocl  8781  3ecoptocl  8782  undifixp  8907  xpdom2  9036  xpf1o  9103  infensuc  9119  findcard2  9128  php  9171  isinf  9207  isinfOLD  9208  unblem2  9240  fodomfir  9279  infssuni  9297  finsschain  9310  fsuppunfi  9339  fsuppunbi  9340  marypha1  9385  hartogs  9497  card2on  9507  card2inf  9508  xpwdomg  9538  elirrv  9549  en3lp  9567  preleqg  9568  inf3lem1  9581  inf3lem2  9582  inf3lem3  9583  inf3lem5  9585  noinfep  9613  ttrclss  9673  ttrclselem2  9679  trcl  9681  tcel  9698  frr3g  9709  rankonidlem  9781  scottex  9838  djuunxp  9874  eldju2ndl  9877  updjud  9887  dif1card  9963  fodomnum  10010  cardaleph  10042  kmlem9  10112  kmlem13  10116  cflim2  10216  cfsmolem  10223  infpssrlem3  10258  isfin7-2  10349  fin1a2lem6  10358  fin1a2lem12  10364  domtriomlem  10395  axdc3lem4  10406  axdc4lem  10408  zorn2lem3  10451  zorn2lem4  10452  zorn2lem5  10453  zorn2lem7  10455  zornn0g  10458  axdclem2  10473  ondomon  10516  alephval2  10525  cfpwsdom  10537  wuncval2  10700  grupr  10750  gruiun  10752  ingru  10768  grothomex  10782  indpi  10860  nqereu  10882  prlem934  10986  reclem2pr  11001  mulgt0sr  11058  supsrlem  11064  1re  11174  dedekind  11337  lemul1a  12036  squeeze0  12086  peano5nni  12189  nnunb  12438  nn0lt2  12597  nn0le2is012  12598  fzind  12632  nn0ind-raph  12634  zindd  12635  eluzaddOLD  12828  uzin  12833  nn01to3  12900  xnn0xadd0  13207  xmulasslem  13245  icoshft  13434  fzen  13502  uzsubsubfz  13507  elfz0ubfz0  13593  elfz0fzfz0  13594  fz0fzelfz0  13595  elfzmlbp  13600  elfzodifsumelfzo  13692  ssfzo12bi  13722  fzoopth  13723  elfzonelfzo  13730  elfznelfzo  13733  injresinjlem  13748  injresinj  13749  modfzo0difsn  13908  modsumfzodifsn  13909  addmodlteq  13911  ssnn0fi  13950  fsuppmapnn0fiub0  13958  expcllem  14037  expeq0  14057  mulexp  14066  leexp2r  14139  bernneq  14194  facdiv  14252  hasheqf1oi  14316  hashnn0n0nn  14356  hashss  14374  hashgt12el  14387  hashgt12el2  14388  hashimarni  14406  hashle2pr  14442  pr2pwpr  14444  hashge2el2dif  14445  hashge2el2difr  14446  hashtpg  14450  hashge3el3dif  14452  exprelprel  14455  hash1to3  14457  hash3tpde  14458  tpfo  14465  fundmge2nop0  14467  fi1uzind  14472  ccatsymb  14547  swrdnd  14619  swrdnd2  14620  swrdnnn0nd  14621  swrdnd0  14622  pfxnd0  14653  swrdswrdlem  14669  swrdswrd  14670  pfxccatin12lem2a  14692  pfxccatin12lem1  14693  swrdccatin2  14694  pfxccatin12lem2  14696  pfxccatin12lem3  14697  pfxccat3  14699  swrdccat  14700  swrdccat3blem  14704  repsdf2  14743  repswswrd  14749  cshwidxmod  14768  cshwidx0  14771  cshf1  14775  cshweqrep  14786  cshw1  14787  cshwsexaOLD  14790  2cshwcshw  14791  scshwfzeqfzo  14792  cshwcsh2id  14794  wwlktovfo  14924  relexpaddg  15019  iseraltlem2  15649  modfsummods  15759  clim2prod  15854  prodfn0  15860  prodfrec  15861  prodmo  15902  fprodabs  15940  binomfallfac  16007  fprodefsum  16061  dvdsaddre2b  16277  addmodlteqALT  16295  oddge22np1  16319  nn0enne  16347  nn0o1gt2  16351  sumeven  16357  sumodd  16358  dvdslegcd  16474  gcdneg  16492  dfgcd2  16516  rplpwr  16528  lcmf  16603  lcmftp  16606  lcmfunsnlem2lem1  16608  lcmfunsnlem2  16610  lcmfdvdsb  16613  coprmdvds1  16622  qredeq  16627  coprmprod  16631  coprmproddvdslem  16632  cncongr1  16637  cncongr2  16638  prm2orodd  16661  2mulprm  16663  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  17504  mreiincl  17557  mreexexd  17609  inveq  17736  cicsym  17766  cictr  17767  initoid  17963  termoid  17964  initoeu2lem0  17975  initoeu2lem1  17976  initoeu2lem2  17977  initoeu2  17978  fthestrcsetc  18111  fthsetcestrc  18126  drsdirfi  18266  isnmgm  18571  mgmhmlin  18626  issubmgm2  18630  sgrpass  18652  insubm  18745  mgm2nsgrplem3  18847  dfgrp3lem  18970  cyccom  19135  symg2bas  19323  symgfix2  19346  symgextf1  19351  gsmsymgrfix  19358  pmtrprfv3  19384  psgnunilem4  19427  efgi2  19655  0ringnnzr  20434  rnghmsscmap  20539  rnghmsubcsetclem2  20541  rngcinv  20546  funcrngcsetc  20549  funcrngcsetcALT  20550  rhmsscmap  20568  rhmsubcsetclem2  20570  rhmsubcrngclem2  20576  ringcbasbas  20582  funcringcsetc  20583  rhmsubclem4  20597  rngqiprngimfo  21211  psgndiflemB  21509  psgndiflemA  21510  elfrlmbasn0  21672  lmictra  21754  mpfrcl  21992  gsummoncoe1  22195  mamufacex  22283  matecl  22312  dmatelnd  22383  dmatscmcl  22390  scmateALT  22399  scmatsgrp1  22409  scmatf1  22418  mavmulsolcl  22438  cramerimplem1  22570  cramerimplem2  22571  pmatcollpw3fi1  22675  mp2pm2mplem4  22696  pm2mpfo  22701  chmaidscmat  22735  fvmptnn04ifb  22738  chfacfscmul0  22745  chfacfpmmul0  22749  cayhamlem1  22753  cayhamlem3  22774  cayleyhamilton1  22779  fiinopn  22788  tgcl  22856  distop  22882  isclo2  22975  iscldtop  22982  ssnei2  23003  opnnei  23007  pnfnei  23107  mnfnei  23108  tgcnp  23140  cnpnei  23151  1stcelcls  23348  txcnpi  23495  cnmptcom  23565  fbfinnfr  23728  isfildlem  23744  snfil  23751  fbunfip  23756  fgcl  23765  elfm2  23835  fmco  23848  fbflim2  23864  cnpflf2  23887  flimfcls  23913  tmdgsum  23982  neibl  24389  tngngpim  24547  fgcfil  25171  caubl  25208  volsuplem  25456  ellimc3  25780  dvnadd  25831  dvnres  25833  cpnord  25837  dvnfre  25856  ply1divex  26042  cxpmul2  26598  fsumdvdsmul  27105  zabsle1  27207  gausslemma2dlem1a  27276  gausslemma2dlem3  27279  lgsquad2lem2  27296  2lgs  27318  2sq2  27344  2sqnn0  27349  2sqnn  27350  2sqreultlem  27358  2sqreunnltlem  27361  qabvexp  27537  sltval2  27568  nolt02o  27607  ssltun1  27720  scutun12  27722  madebday  27811  mulsprop  28033  precsexlem8  28116  precsexlem9  28117  noseqind  28186  om2noseqrdg  28198  n0cutlt  28249  peano5uzs  28292  expadds  28320  axcontlem4  28894  umgredgprv  29034  umgrnloop  29035  upgrpredgv  29066  upgredgpr  29069  edglnl  29070  usgredgprvALT  29122  usgrnloopALT  29130  usgredg2v  29154  fusgrfis  29257  nbuhgr2vtx1edgblem  29278  nb3grprlem1  29307  cusgrsize2inds  29381  cusgrfi  29386  fusgrn0degnn0  29427  uspgrloopvtxel  29444  vtxdginducedm1lem4  29470  uhgr0edg0rgrb  29502  wlkl1loop  29566  wlk1walk  29567  upgriswlk  29569  upgrwlkvtxedg  29573  uspgr2wlkeq  29574  wlkv0  29579  wlksoneq1eq2  29592  wlkon2n0  29594  wlkreslem  29597  wlkres  29598  lfgrwlkprop  29615  pthdivtx  29657  2pthnloop  29661  spthonepeq  29682  uhgrwkspthlem2  29684  uhgrwkspth  29685  usgr2wlkneq  29686  usgr2trlncl  29690  usgr2pthlem  29693  usgr2pth  29694  cyclnspth  29731  lfgrn1cycl  29735  usgr2trlncrct  29736  uspgrn2crct  29738  crctcshwlkn0lem3  29742  crctcshwlkn0lem5  29744  wwlknp  29773  wspthneq1eq2  29790  0enwwlksnge1  29794  wlklnwwlkln1  29798  wlkiswwlks2  29805  wlkiswwlksupgr2  29807  wlklnwwlkln2lem  29812  wwlksnred  29822  wwlksnextbi  29824  wwlksnredwwlkn0  29826  wwlksnextwrd  29827  wwlksnextinj  29829  wwlksnextproplem3  29841  wwlksnextprop  29842  wspthsnwspthsnon  29846  wspthsnonn0vne  29847  2pthon3v  29873  umgr2adedgwlkonALT  29877  umgr2wlk  29879  umgr2wlkon  29880  umgrwwlks2on  29887  elwspths2on  29890  usgr2wspthons3  29894  elwwlks2  29896  rusgrnumwwlk  29905  clwwlkccatlem  29918  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwlkclwwlklem2  29929  clwlkclwwlkf1lem3  29935  erclwwlkeqlen  29948  clwwlknwwlksn  29967  loopclwwlkn1b  29971  clwwlkf1  29978  wwlksext2clwwlk  29986  eleclclwwlknlem2  29990  umgr2cwwk2dif  29993  eleclclwwlkn  30005  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  clwwlknonwwlknonb  30035  clwwlknonex2lem2  30037  clwwlknonex2  30038  1pthon2v  30082  upgr3v3e3cycl  30109  uhgr3cyclexlem  30110  uhgr3cyclex  30111  eupth2lem3lem4  30160  frgr3vlem1  30202  frgr3vlem2  30203  3vfriswmgrlem  30206  3vfriswmgr  30207  3cyclfrgrrn1  30214  n4cyclfrgr  30220  frgrncvvdeqlem3  30230  frgrncvvdeqlem6  30233  frgrncvvdeqlem7  30234  frgrncvvdeqlem8  30235  frgrwopreglem4a  30239  frgrwopreglem3  30243  frgrwopreg1  30247  frgrwopreg2  30248  frgrwopreglem5lem  30249  frgrwopreglem5ALT  30251  frgrwopreg  30252  fusgr2wsp2nb  30263  2wspmdisj  30266  numclwwlk1lem2foa  30283  numclwwlk1lem2f1  30286  numclwwlk1lem2fo  30287  numclwwlk1  30290  wlkl0  30296  numclwwlk2lem1  30305  numclwlk2lem2f  30306  numclwlk2lem2f1o  30308  frgrreg  30323  frgrregord013  30324  frgrregord13  30325  friendshipgt3  30327  friendship  30328  eulplig  30414  ipassi  30770  ubthlem2  30800  isch3  31170  shintcli  31258  shmodsi  31318  spansncvi  31581  hoaddsub  31745  eigorthi  31766  pjss2coi  32093  pjnormssi  32097  pj3cor1i  32138  strb  32187  dmdmd  32229  mdsl0  32239  csmdsymi  32263  chrelat2i  32294  mdsymlem3  32334  mdsymlem6  32337  sumdmdlem2  32348  opreu2reuALT  32406  ssrelf  32543  gsumwun  33005  onvf1odlem4  35093  spthcycl  35116  loop1cycl  35124  cvmlift2lem1  35289  satfrel  35354  satfrnmapom  35357  fmlafvel  35372  fmla1  35374  gonarlem  35381  gonar  35382  goalrlem  35383  goalr  35384  satffunlem  35388  satffunlem1lem1  35389  satffunlem2lem1  35391  satffun  35396  satefvfmla1  35412  mrsubvrs  35509  mclsax  35556  3ccased  35706  dfon2lem3  35773  rdgprc  35782  cgrextend  35996  btwndiff  36015  btwnconn1lem12  36086  brsegle  36096  broutsideof2  36110  funray  36128  in-ax8  36212  ss-ax8  36213  elicc3  36305  nn0prpwlem  36310  nn0prpw  36311  fnessref  36345  neibastop2lem  36348  filnetlem4  36369  meran1  36399  waj-ax  36402  arg-ax  36404  bj-nnclavc  36536  bj-con2com  36549  bj-axdd2  36580  bj-alrimg  36607  bj-exlimg  36611  bj-exalimi  36621  bj-cbvalimt  36627  bj-eximcom  36631  bj-ssbid1ALT  36653  bj-sb  36675  bj-snsetex  36951  bj-restpw  37080  bj-finsumval0  37273  mptsnunlem  37326  icoreclin  37345  relowlpssretop  37352  inunissunidif  37363  rdgssun  37366  finorwe  37370  domalom  37392  wl-dral1d  37519  wl-exeq  37522  wl-lem-exsb  37554  poimirlem29  37643  poimirlem32  37646  fdc  37739  seqpo  37741  incsequz  37742  isismty  37795  ismtybndlem  37800  heibor1lem  37803  ismgmOLD  37844  isexid2  37849  ghomco  37885  pridlc  38065  relcnveq3  38309  elrelscnveq3  38482  cdleme18d  40289  tendovalco  40759  cdlemn11pre  41204  dihord2pre  41219  indstrd  42181  unitscyglem3  42185  nnadddir  42258  eu6w  42664  incssnn0  42699  fphpd  42804  jm2.19lem3  42980  setindtr  43013  islssfg2  43060  mpaaeu  43139  ordnexbtwnsuc  43256  oaabsb  43283  succlg  43317  oacl2g  43319  omabs2  43321  omcl2  43322  omcl3g  43323  pr2cv  43537  refimssco  43596  iunrelexpmin1  43697  iunrelexpmin2  43701  trclimalb2  43715  clsk1indlem3  44032  tfindsd  44199  mnurndlem1  44270  nzss  44306  sb5ALT  44515  truniALT  44531  ee223  44624  3orbi123VD  44839  sbc3orgVD  44840  exbirVD  44842  exbiriVD  44843  sbcim2gVD  44864  trsbcVD  44866  truniALTVD  44867  onfrALTlem3VD  44876  onfrALTlem2VD  44878  csbrngVD  44885  19.41rgVD  44891  ax6e2eqVD  44896  ax6e2ndeqVD  44898  2uasbanhVD  44900  sb5ALTVD  44902  vk15.4jVD  44903  infxrunb3rnmpt  45424  stoweidlem26  46024  et-equeucl  46870  hirstL-ax3  46893  rexsb  47100  rexrsb  47101  euoreqb  47110  2reu8i  47114  afvres  47173  tz6.12-afv  47174  afvco2  47177  afv2orxorb  47229  afv2res  47240  tz6.12-afv2  47241  tz6.12i-afv2  47244  dfatcolem  47256  zm1nn  47303  2ffzoeq  47328  smonoord  47372  iccpartiltu  47423  iccpartlt  47425  iccpartltu  47426  iccpartgtl  47427  iccpartgt  47428  iccpartleu  47429  iccpartgel  47430  icceuelpart  47437  iccpartnel  47439  lswn0  47445  ichnreuop  47473  ichreuopeq  47474  prsprel  47488  sprsymrelfvlem  47491  sprsymrelf1lem  47492  sprsymrelfolem2  47494  prproropf1olem4  47507  paireqne  47512  prprelb  47517  reupr  47523  goldbachth  47548  odz2prm2pw  47564  fmtno4prmfac  47573  fmtno4prmfac193  47574  prmdvdsfmtnof1lem2  47586  2pwp1prmfmtno  47591  lighneallem2  47607  lighneallem4b  47610  lighneallem4  47611  requad2  47624  odd2prm2  47719  mogoldbblem  47721  gbepos  47759  gbowgt5  47763  gbowge7  47764  stgoldbwt  47777  sbgoldbwt  47778  sbgoldbst  47779  sbgoldbaltlem1  47780  sbgoldbalt  47782  sbgoldbo  47788  nnsum3primesle9  47795  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  bgoldbtbndlem1  47806  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbnd  47810  dfnbgr6  47857  isuspgrimlem  47895  uhgrimisgrgric  47931  clnbgrgrim  47934  usgrgrtrirex  47949  isubgr3stgrlem4  47968  grilcbri2  48003  grlicsym  48005  grlictr  48007  gricgrlic  48010  gpgvtxedg0  48054  gpgvtxedg1  48055  gpgedg2ov  48057  gpgedg2iv  48058  pgnioedg1  48098  pgnioedg2  48099  pgnioedg3  48100  pgnioedg4  48101  pgnioedg5  48102  pgnbgreunbgrlem2lem3  48106  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem5lem1  48110  pgnbgreunbgrlem5lem2  48111  pgnbgreunbgrlem5lem3  48112  pgnbgreunbgrlem6  48114  upgrwlkupwlk  48128  uspgrsprf1  48135  lmod0rng  48217  lidldomn1  48219  rngccatidALTV  48260  rngcinvALTV  48264  rhmsubcALTVlem4  48272  funcringcsetcALTV2lem9  48286  ringccatidALTV  48294  ringcbasbasALTV  48300  ztprmneprm  48335  pgrpgt2nabl  48354  lmodvsmdi  48367  ply1mulgsumlem2  48376  lincsumcl  48420  ellcoellss  48424  linindslinci  48437  islinindfis  48438  lincext3  48445  lindslinindimp2lem4  48450  lindslinindsimp2lem5  48451  lindslinindsimp2  48452  lindsrng01  48457  ldepspr  48462  lincresunit3lem1  48468  elfzolborelfzop1  48508  dignn0ldlem  48591  nn0sumshdiglem1  48610  1arymaptf1  48631  2arymaptf1  48642  rrx2xpref1o  48707  rrx2plord2  48711  rrx2plordisom  48712  line2ylem  48740  line2xlem  48742  line2y  48744  itschlc0xyqsol1  48755  inlinecirc02plem  48775  fullthinc  49439  tfis2d  49669  onsetrec  49697