MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com12 Unicode version

Theorem com12 27
Description: Inference that swaps (commutes) antecedents in an implication. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)
Hypothesis
Ref Expression
com12.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
com12  |-  ( ps 
->  ( ph  ->  ch ) )

Proof of Theorem com12
StepHypRef Expression
1 id 19 . 2  |-  ( ps 
->  ps )
2 com12.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5com 26 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl5  28  syl6com  31  mpcom  32  syli  33  pm2.27  35  pm2.43b  46  syl9r  67  com3r  73  pm2.86i  92  pm2.24  100  con3rr3  126  expt  146  jad  152  pm2.61  161  syl5ibcom  209  syl5ibrcom  211  pm5.501  328  jaod  367  orel1  369  pm2.62  396  impcom  416  imp3a  417  expcom  421  exp3a  422  pm3.21  430  imdistanri  667  pm2.64  728  pm2.75  786  ccased  879  dedlem0b  885  3impd  1130  3expd  1133  mp3an1i  1234  simplbi2com  1315  meredith  1319  ax12olem21  1565  ax12olem23  1567  ax10lem16  1575  ax10lem26  1585  ax10  1587  hbimd  1680  19.21t  1683  equtrr  1701  sbequ2  1755  ax11b  1801  sb6rf  1843  sb56  1849  exmoeu  2003  moimv  2009  eupickbi  2027  2eu1  2041  exists2  2051  r19.12  2415  2gencl  2540  3gencl  2541  rcla4cv  2595  ceqex  2610  mob  2667  euind  2672  reuind  2686  sseq2  2873  uneqdifeq  3197  difsn  3402  eqsn  3420  preq12b  3433  intab  3532  iinss2  3593  trint0  3734  dtru  3802  sspwb  3822  copsexg  3850  pocl  3916  pofun  3925  solin  3932  frss  3955  tz7.7  4013  ordtri3  4023  ordtr2  4031  suc11  4089  onssneli  4095  eusv2  4139  ralxfrALT  4163  iunpw  4181  ordom  4276  limom  4282  peano5  4290  2optocl  4392  3optocl  4393  ssrel  4403  ssrelrel  4413  relop  4460  xpidtr  4690  trin2  4691  sotri3  4698  poltletr  4703  xp11  4736  relcnvtr  4816  funmo  4845  fss  4969  fv3  5104  tz6.12-1  5107  tz6.12c  5111  tz6.12i  5112  mpteqb  5174  fornex  5243  funfvima  5309  fvclss  5316  f1fveq  5341  isotr  5381  isotrALT  5382  isoselem  5387  oprabid  5428  ovg  5525  poxp  5756  soxp  5757  tposfn2  5783  sorpsscmpl  5811  iotaval  5825  onnseq  5860  smores  5868  smoel  5876  smogt  5883  smoiso2  5885  tfrlem2  5891  tfr3  5914  tz7.48-2  5953  tz7.48-3  5955  tz7.49  5956  abianfp  5970  oecl  6035  oaordex  6055  oalimcl  6057  oaass  6058  omordi  6063  omlimcl  6075  odi  6076  omeulem1  6079  oen0  6083  oewordri  6089  nnawordi  6118  nnaass  6119  nnmordi  6128  omabs  6144  omsmolem  6150  iiner  6230  2ecoptocl  6238  3ecoptocl  6239  th3qlem2  6254  undifixp  6334  xpdom2  6438  xpf1o  6551  infensuc  6567  php  6573  onomeneq  6578  isinf  6603  findcard2  6625  unblem2  6637  finsschain  6688  marypha1  6713  supub  6734  suplub  6735  supsnALT  6750  hartogs  6786  card2on  6795  card2inf  6796  xpwdomg  6826  elirrv  6838  inf3lem1  6856  inf3lem2  6857  inf3lem3  6858  inf3lem5  6860  noinfep  6887  noinfepOLD  6888  trcl  6937  en3lp  6945  tcel  6957  r1sdom  6973  rankonidlem  7026  scottex  7081  pr2ne  7161  dif1card  7164  fodomnum  7210  cardaleph  7242  cflim2  7396  cfsmolem  7403  infpssrlem3  7438  isfin7-2  7529  fin1a2lem6  7538  fin1a2lem10  7542  fin1a2lem12  7544  domtriomlem  7575  axdc3lem4  7586  axdc4lem  7588  kmlem4  7626  kmlem9  7631  kmlem12  7634  kmlem13  7635  zorn2lem3  7645  zorn2lem4  7646  zorn2lem5  7647  zorn2lem6  7648  zorn2lem7  7649  zornn0g  7652  axdclem  7666  axdclem2  7667  ondomon  7703  alephval2  7710  cfpwsdom  7722  axrepnd  7732  tskr1om  7857  grupr  7885  gruiun  7887  ingru  7902  grothomex  7916  indpi  7996  nqereu  8018  genpnnp  8094  prlem934  8122  ltaddpr2  8124  reclem2pr  8137  mulgt0sr  8192  supsrlem  8198  lemul1a  9036  squeeze0  9085  peano5nni  9174  nnunb  9383  fzind  9531  nn0ind-raph  9534  zindd  9535  eluzadd  9678  uzin  9682  xmulasslem  10026  icoshft  10176  fzen  10227  expcllem  10522  expeq0  10540  mulexp  10549  leexp2r  10567  bernneq  10634  facdiv  10707  hashmap  10793  cjexp  10883  absexp  11035  iseraltlem2  11400  sin01gt0  11707  alzdvds  11814  dvdslegcd  11854  gcdneg  11864  rplpwr  11894  qredeq  11944  prmpwdvds  12110  prmreclem4  12125  ramcl  12235  imasleval  12582  mreiincl  12635  drsdirfi  12687  spwmo  12941  efgi2  13798  fiinopn  15408  tgcl  15468  distop  15494  isclo2  15585  iscldtop  15592  ssnei2  15613  opnnei  15617  pnfnei  15696  mnfnei  15697  tgcnp  15729  cnpnei  15739  2ndcctbss  15923  1stcelcls  15929  txcnpi  16044  cnmptcom  16114  fbfinnfr  16278  isfildlem  16294  snfil  16301  fbunfip  16306  fgcl  16315  elfm2  16385  fmfnfmlem1  16391  fmco  16398  fbflim2  16414  flffbas  16432  cnpflf2  16437  flimfcls  16463  tmdgsum  16520  neibl  16790  metcnp3  16829  fgcfil  17432  caubl  17468  volsuplem  17647  dvnadd  17989  dvnres  17990  cpnord  17994  mpfrcl  18102  ply1divex  18220  cxpmul2  18681  wilthlem3  18917  lgsquad2lem2  19207  qabvexp  19384  gxnn0add  19532  gxnn0mul  19535  ismgm  19578  isexid2  19583  ipassi  20010  ubthlem2  20041  isch3  20412  shintcli  20499  shmodsi  20559  spansncvi  20840  pjjsi  20888  hoaddsub  20987  eigorthi  21008  pjss2coi  21335  pjnormssi  21339  pj3cor1i  21380  strb  21429  dmdmd  21471  mdsl0  21481  csmdsymi  21505  chrelat2i  21536  cvati  21537  mdsymlem3  21576  mdsymlem6  21579  sumdmdlem2  21590  dmdbr5ati  21593  cvmlift2lem1  21765  3ccased  22008  dedekind  22012  dfres3  22044  dfon2lem3  22067  rdgprc  22077  trpredmintr  22161  trpredrec  22168  wfr3g  22182  wfrlem12  22194  frr3g  22207  frrlem11  22220  sltval2  22236  axfelem13  22285  elfuns  22387  axcontlem4  22528  cgrextend  22564  btwndiff  22583  btwnconn1lem12  22654  brsegle  22664  broutsideof2  22678  funray  22696  meran1  22758  waj-ax  22761  arg-ax  22763  wl-pm2.86i  22829  copsexgb  22866  evpexun  22895  isunscov  22955  restidsing  22957  twsymr  22959  prj1b  22960  prj3  22961  fixpc  22975  domintrefc  23007  mapmapmap  23032  injsurinj  23033  repfuntw  23044  cbcpcp  23046  prl  23051  prl2  23053  prjmapcp2  23054  dstr  23055  jidd  23076  midd  23077  int2pre  23121  ubpar  23145  inposet  23162  tolat  23170  toplat  23174  latdir  23179  ridlideq  23219  rzrlzreq  23220  resgcom  23235  grpodivone  23257  grpodivfo  23258  rltrran  23298  zerdivemp1  23320  muldisc  23368  svli2  23371  svs2  23374  truni1  23392  truni2  23393  truni3  23394  inttop2  23405  nsn  23420  intopcoaconlem3b  23428  intopcoaconc  23431  qusp  23432  intcont  23433  prcnt  23441  fisub  23444  cmptdst  23458  exopcopn  23462  prdnei  23463  limptlimpr2lem1  23464  limptlimpr2lem2  23465  islimrs  23470  islimrs3  23471  islimrs4  23472  bwt2  23482  iintlem1  23500  iint  23502  lvsovso  23516  supnuf  23519  claddrvr  23538  sigadd  23539  addcomv  23545  addcanrg  23557  negveudr  23559  subclrvd  23564  distsava  23579  intvconlem1  23593  hdrmp  23596  cmppfd  23635  domcmpd  23636  codcmpd  23637  cmpasso  23663  cmpida  23664  cmpidb  23665  cmpassoh  23691  homgrf  23692  imonclem  23703  cmpmon  23705  iepiclem  23713  isepic  23714  idfisf  23731  issrc  23757  propsrc  23758  partarelt1  23786  inttarcar  23791  fnctartar  23797  fnctartar2  23798  prismorcset2  23808  cmpmor  23865  setiscat  23869  lemindclsbu  23886  indcls2  23887  clscnc  23901  pgapspf2  23944  gltpntl  23963  lineval5a  23979  lineval6a  23980  isconcl5a  23993  isconcl5ab  23994  isconcl6a  23995  isibg2aa  24004  isib2g1a1  24008  isibg1a2  24009  isibg2a  24010  isibg1a3a  24014  isibg1a4a  24015  isibg1a5a  24016  bsstr  24020  nbssntr  24021  sgplpte21d  24028  segline  24033  pxysxy  24034  lppotoslem  24035  lppotos  24036  xsyysx  24037  nbssntrs  24039  pdiveql  24060  abhp  24065  elicc3  24121  nn0prpwlem  24131  nn0prpw  24132  fnessref  24186  neibastop2lem  24202  filnetlem4  24223  fzmul  24337  fdc  24349  seqpo  24351  incsequz  24352  isismty  24419  ismtybndlem  24424  heibor1lem  24427  ghomco  24467  zerdivemp1x  24480  pridlc  24590  ceqsex3OLD  24620  nelss  24645  incssnn0  24682  fphpd  24792  jm2.19lem3  24977  setindtr  25010  dfac21  25061  aalioulem2  25075  islssfg2  25105  mpaaeu  25291  psgnunilem4  25356  pm14.24  25570  hirstL-ax3  25623  sb5ALT  25739  truniALT  25756  onfrALTlem3  25760  ee223  25853  3orbi123VD  26026  sbc3orgVD  26027  exbirVD  26029  exbiriVD  26030  sbcim2gVD  26051  trsbcVD  26053  truniALTVD  26054  onfrALTlem3VD  26063  onfrALTlem2VD  26065  csbrngVD  26072  19.41rgVD  26078  a9e2eqVD  26083  a9e2ndeqVD  26085  2uasbanhVD  26087  sb5ALTVD  26089  vk15.4jVD  26090  ax12-3  26507  ax9lem2  26544  ax9lem5  26547  ax9lem15  26557  ax9vax9  26561  cdleme18d  27887  tendovalco  28357  cdlemn11pre  28803  dihord2pre  28818
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator