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  101  con3rr3  128  expt  148  jad  154  pm2.61  163  syl5ibcom  211  syl5ibrcom  213  pm5.501  330  jaod  369  orel1  371  pm2.62  398  impcom  419  imp3a  420  expcom  424  exp3a  425  pm3.21  435  imdistanri  672  pm2.64  764  pm2.75  822  ccased  913  dedlem0b  919  3impd  1165  3expd  1168  mp3an1i  1270  simplbi2com  1364  meredith  1394  sbequ2  1632  equtrr  1654  ax12olem1  1870  ax12olem3  1872  ax10lem4  1883  ax11b  1938  sb6rf  2030  sb56  2037  exsb  2072  mo  2166  exmoeu  2186  morimv  2192  eupickbi  2210  2mo  2222  2eu1  2224  exists2  2234  r19.12  2657  2gencl  2818  3gencl  2819  rspccv  2882  ceqex  2899  mob  2948  euind  2953  reuind  2969  2rmorex  2970  sseq2  3201  reupick2  3455  uneqdifeq  3543  difsn  3756  eqsn  3776  preq12b  3789  iinss2  3955  disjxiun  4021  trint0  4131  dtru  4200  sspwb  4222  copsexg  4251  pocl  4320  pofun  4329  solin  4336  frss  4359  tz7.7  4417  ordtri3  4427  ordtr2  4435  suc11  4495  onssneli  4501  reusv1  4533  reusv2lem1  4534  alxfr  4546  ralxfrALT  4552  iunpw  4569  ordom  4664  limom  4670  peano5  4678  2optocl  4764  3optocl  4765  ssrel  4775  ssrelrel  4786  relop  4833  asymref2  5059  xpidtr  5064  trin2  5065  sotri3  5072  poltletr  5077  xp11  5110  relcnvtr  5190  funmo  5237  fss  5363  fv3  5502  tz6.12-1  5505  tz6.12c  5509  tz6.12i  5510  mpteqb  5576  fornex  5712  funfvima  5715  fvclss  5722  f1fveq  5748  isoselem  5800  oprabid  5844  ovg  5948  poxp  6189  soxp  6190  tposfn2  6218  sorpsscmpl  6250  iotaval  6264  onnseq  6357  smoel  6373  smogt  6380  smoiso2  6382  tfrlem2  6388  tfr3  6411  tz7.48-2  6450  tz7.48-3  6452  tz7.49  6453  abianfp  6467  oecl  6532  oaordex  6552  oalimcl  6554  oaass  6555  omordi  6560  omlimcl  6572  odi  6573  omeulem1  6576  oen0  6580  oewordri  6586  nnawordi  6615  nnaass  6616  nnmordi  6625  omabs  6641  omsmolem  6647  iiner  6727  2ecoptocl  6745  3ecoptocl  6746  th3qlem2  6761  undifixp  6848  xpdom2  6953  xpf1o  7019  infensuc  7035  php  7041  onomeneq  7046  isinf  7072  findcard2  7094  unblem2  7106  finsschain  7158  marypha1  7183  hartogs  7255  card2on  7264  card2inf  7265  xpwdomg  7295  elirrv  7307  inf3lem1  7325  inf3lem2  7326  inf3lem3  7327  inf3lem5  7329  noinfep  7356  noinfepOLD  7357  trcl  7406  en3lp  7414  tcel  7426  r1sdom  7442  rankonidlem  7496  scottex  7551  pr2ne  7631  dif1card  7634  fodomnum  7680  cardaleph  7712  kmlem4  7775  kmlem9  7780  kmlem12  7783  kmlem13  7784  cflim2  7885  cfsmolem  7892  infpssrlem3  7927  isfin7-2  8018  fin1a2lem6  8027  fin1a2lem10  8031  fin1a2lem12  8033  domtriomlem  8064  axdc3lem4  8075  axdc4lem  8077  zorn2lem3  8121  zorn2lem4  8122  zorn2lem5  8123  zorn2lem6  8124  zorn2lem7  8125  zornn0g  8128  axdclem  8142  axdclem2  8143  ondomon  8181  alephval2  8190  cfpwsdom  8202  wunr1om  8337  wuncval2  8365  tskr1om  8385  grupr  8415  gruiun  8417  ingru  8433  grothomex  8447  indpi  8527  nqereu  8549  genpnnp  8625  prlem934  8653  ltaddpr2  8655  reclem2pr  8668  mulgt0sr  8723  supsrlem  8729  lemul1a  9606  squeeze0  9655  peano5nni  9745  nnunb  9957  fzind  10105  nn0ind-raph  10108  zindd  10109  eluzadd  10252  uzin  10256  xmulasslem  10601  icoshft  10754  fzen  10807  expcllem  11110  expeq0  11128  mulexp  11137  leexp2r  11155  bernneq  11223  facdiv  11296  hashmap  11383  cjexp  11631  absexp  11785  iseraltlem2  12151  sin01gt0  12466  alzdvds  12574  dvdslegcd  12691  gcdneg  12701  rplpwr  12731  qredeq  12781  prmpwdvds  12947  prmreclem4  12962  ramcl  13072  imasleval  13439  mreiincl  13494  mreexexd  13546  drsdirfi  14068  spwmo  14331  efgi2  15030  fiinopn  16643  tgcl  16703  distop  16729  isclo2  16821  iscldtop  16828  ssnei2  16849  opnnei  16853  pnfnei  16946  mnfnei  16947  tgcnp  16979  cnpnei  16989  2ndcctbss  17177  1stcelcls  17183  txcnpi  17298  cnmptcom  17368  fbfinnfr  17532  isfildlem  17548  snfil  17555  fbunfip  17560  fgcl  17569  elfm2  17639  fmfnfmlem1  17645  fmco  17652  fbflim2  17668  flffbas  17686  cnpflf2  17691  flimfcls  17717  tmdgsum  17774  neibl  18043  metcnp3  18082  fgcfil  18693  caubl  18729  volsuplem  18908  ellimc3  19225  dvnadd  19274  dvnres  19276  cpnord  19280  dvnfre  19297  mpfrcl  19398  ply1divex  19518  aalioulem2  19709  cxpmul2  20032  wilthlem3  20304  lgsquad2lem2  20594  qabvexp  20771  gxnn0add  20935  gxnn0mul  20938  ismgm  20981  isexid2  20986  ipassi  21413  ubthlem2  21444  isch3  21817  shintcli  21904  shmodsi  21964  spansncvi  22227  pjjsi  22275  hoaddsub  22392  eigorthi  22413  pjss2coi  22740  pjnormssi  22744  pj3cor1i  22785  strb  22834  dmdmd  22876  mdsl0  22886  csmdsymi  22910  chrelat2i  22941  cvati  22942  mdsymlem3  22981  mdsymlem6  22984  sumdmdlem2  22995  dmdbr5ati  22998  cvmlift2lem1  23240  3ccased  23480  dedekind  23488  dfres3  23522  dfon2lem3  23545  rdgprc  23555  trpredmintr  23638  trpredrec  23645  wfr3g  23659  wfrlem12  23671  frr3g  23684  frrlem11  23697  sltval2  23713  axfelem13  23762  elfuns  23864  axcontlem4  24005  cgrextend  24041  btwndiff  24060  btwnconn1lem12  24131  brsegle  24141  broutsideof2  24155  funray  24173  meran1  24260  waj-ax  24263  arg-ax  24265  wl-pm2.86i  24331  isunscov  24484  restidsing  24486  twsymr  24488  prj1b  24489  prj3  24490  fixpc  24504  domintrefc  24536  mapmapmap  24559  injsurinj  24560  repfuntw  24571  cbcpcp  24573  prl  24578  prl2  24580  prjmapcp2  24581  dstr  24582  jidd  24603  midd  24604  int2pre  24648  ubpar  24672  inposet  24689  tolat  24697  toplat  24701  latdir  24706  ridlideq  24746  rzrlzreq  24747  resgcom  24762  grpodivone  24784  grpodivfo  24785  rltrran  24825  zerdivemp1  24847  muldisc  24892  svli2  24895  svs2  24898  truni1  24916  truni2  24917  truni3  24918  inttop2  24926  nsn  24941  intopcoaconlem3b  24949  intopcoaconc  24952  qusp  24953  intcont  24954  prcnt  24962  fisub  24965  cmptdst  24979  exopcopn  24983  prdnei  24984  limptlimpr2lem1  24985  limptlimpr2lem2  24986  islimrs  24991  islimrs3  24992  islimrs4  24993  bwt2  25003  iintlem1  25021  iint  25023  lvsovso  25037  supnuf  25040  claddrvr  25059  sigadd  25060  addcomv  25066  addcanrg  25078  negveudr  25080  subclrvd  25085  distsava  25100  intvconlem1  25114  hdrmp  25117  cmppfd  25156  domcmpd  25157  codcmpd  25158  cmpasso  25184  cmpida  25185  cmpidb  25186  cmpassoh  25212  homgrf  25213  imonclem  25224  cmpmon  25226  iepiclem  25234  isepic  25235  idfisf  25252  issrc  25278  propsrc  25279  partarelt1  25307  inttarcar  25312  fnctartar  25318  fnctartar2  25319  prismorcset2  25329  cmpmor  25386  setiscat  25390  lemindclsbu  25406  indcls2  25407  clscnc  25421  pgapspf2  25464  gltpntl  25483  lineval5a  25499  lineval6a  25500  isconcl5a  25512  isconcl5ab  25513  isconcl6a  25514  isibg2aa  25523  isib2g1a1  25527  isibg1a2  25528  isibg2a  25529  isibg1a3a  25533  isibg1spa  25534  isibg1a5a  25535  bsstr  25539  nbssntr  25540  sgplpte21d  25547  segline  25552  pxysxy  25553  lppotoslem  25554  lppotos  25555  xsyysx  25556  nbssntrs  25558  pdiveql  25579  abhp  25584  elicc3  25639  nn0prpwlem  25649  nn0prpw  25650  fnessref  25704  neibastop2lem  25720  filnetlem4  25741  fzmul  25854  fdc  25866  seqpo  25868  incsequz  25869  isismty  25936  ismtybndlem  25941  heibor1lem  25944  ghomco  25984  zerdivemp1x  25997  pridlc  26107  ceqsex3OLD  26137  nelss  26162  incssnn0  26197  fphpd  26310  jm2.19lem3  26495  setindtr  26528  dfac21  26575  islssfg2  26580  mpaaeu  26766  psgnunilem4  26831  pm14.24  27043  stoweidlem26  27186  hirstL-ax3  27251  rexsb  27337  rexrsb  27338  2reu1  27355  afvres  27425  tz6.12-afv  27426  afvco2  27428  ndmaovdistr  27458  sb5ALT  27571  truniALT  27588  onfrALTlem3  27592  ee223  27686  3orbi123VD  27906  sbc3orgVD  27907  exbirVD  27909  exbiriVD  27910  sbcim2gVD  27931  trsbcVD  27933  truniALTVD  27934  onfrALTlem3VD  27943  onfrALTlem2VD  27945  csbrngVD  27952  19.41rgVD  27958  a9e2eqVD  27963  a9e2ndeqVD  27965  2uasbanhVD  27967  sb5ALTVD  27969  vk15.4jVD  27970  ax12-3  28383  ax9lem2  28420  ax9lem5  28423  ax9lem15  28433  ax9vax9  28437  cdleme18d  29763  tendovalco  30233  cdlemn11pre  30679  dihord2pre  30694
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator