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  1633  equtrr  1655  ax12olem1  1870  ax12olem3  1872  ax10lem4  1883  ax11b  1937  sb6rf  2033  sb56  2039  exsb  2071  mo  2167  exmoeu  2187  morimv  2193  eupickbi  2211  2mo  2223  2eu1  2225  exists2  2235  r19.12  2658  2gencl  2819  3gencl  2820  rspccv  2883  ceqex  2900  mob  2949  euind  2954  reuind  2970  2rmorex  2971  sseq2  3202  reupick2  3456  uneqdifeq  3544  difsn  3757  eqsn  3777  preq12b  3790  iinss2  3956  disjxiun  4022  trint0  4132  dtru  4203  sspwb  4225  copsexg  4254  pocl  4323  pofun  4332  solin  4339  frss  4362  tz7.7  4420  ordtri3  4430  ordtr2  4438  suc11  4498  onssneli  4504  reusv1  4536  reusv2lem1  4537  alxfr  4549  ralxfrALT  4555  iunpw  4572  ordom  4667  limom  4673  peano5  4681  2optocl  4767  3optocl  4768  ssrel  4778  ssrelrel  4789  relop  4836  asymref2  5062  xpidtr  5067  trin2  5068  sotri3  5075  poltletr  5080  xp11  5113  relcnvtr  5194  iotaval  5232  funmo  5273  fss  5399  fv3  5543  tz6.12c  5549  tz6.12i  5550  mpteqb  5616  fornex  5752  funfvima  5755  fvclss  5762  f1fveq  5788  isoselem  5840  oprabid  5884  ovg  5988  poxp  6229  soxp  6230  tposfn2  6258  sorpsscmpl  6290  onnseq  6363  smoel  6379  smogt  6386  smoiso2  6388  tfrlem2  6394  tfr3  6417  tz7.48-2  6456  tz7.48-3  6458  tz7.49  6459  abianfp  6473  oecl  6538  oaordex  6558  oalimcl  6560  oaass  6561  omordi  6566  omlimcl  6578  odi  6579  omeulem1  6582  oen0  6586  oewordri  6592  nnawordi  6621  nnaass  6622  nnmordi  6631  omabs  6647  omsmolem  6653  iiner  6733  2ecoptocl  6751  3ecoptocl  6752  th3qlem2  6767  undifixp  6854  xpdom2  6959  xpf1o  7025  infensuc  7041  php  7047  onomeneq  7052  isinf  7078  findcard2  7100  unblem2  7112  finsschain  7164  marypha1  7189  hartogs  7261  card2on  7270  card2inf  7271  xpwdomg  7301  elirrv  7313  inf3lem1  7331  inf3lem2  7332  inf3lem3  7333  inf3lem5  7335  noinfep  7362  noinfepOLD  7363  trcl  7412  en3lp  7420  tcel  7432  r1sdom  7448  rankonidlem  7502  scottex  7557  pr2ne  7637  dif1card  7640  fodomnum  7686  cardaleph  7718  kmlem4  7781  kmlem9  7786  kmlem12  7789  kmlem13  7790  cflim2  7891  cfsmolem  7898  infpssrlem3  7933  isfin7-2  8024  fin1a2lem6  8033  fin1a2lem10  8037  fin1a2lem12  8039  domtriomlem  8070  axdc3lem4  8081  axdc4lem  8083  zorn2lem3  8127  zorn2lem4  8128  zorn2lem5  8129  zorn2lem6  8130  zorn2lem7  8131  zornn0g  8134  axdclem  8148  axdclem2  8149  ondomon  8187  alephval2  8196  cfpwsdom  8208  wunr1om  8343  wuncval2  8371  tskr1om  8391  grupr  8421  gruiun  8423  ingru  8439  grothomex  8453  indpi  8533  nqereu  8555  genpnnp  8631  prlem934  8659  ltaddpr2  8661  reclem2pr  8674  mulgt0sr  8729  supsrlem  8735  lemul1a  9612  squeeze0  9661  peano5nni  9751  nnunb  9963  fzind  10112  nn0ind-raph  10114  zindd  10115  eluzadd  10258  uzin  10262  xmulasslem  10607  icoshft  10760  fzen  10813  expcllem  11116  expeq0  11134  mulexp  11143  leexp2r  11161  bernneq  11229  facdiv  11302  hashmap  11389  cjexp  11637  absexp  11791  iseraltlem2  12157  sin01gt0  12472  alzdvds  12580  dvdslegcd  12697  gcdneg  12707  rplpwr  12737  qredeq  12787  prmpwdvds  12953  prmreclem4  12968  ramcl  13078  imasleval  13445  mreiincl  13500  mreexexd  13552  drsdirfi  14074  spwmo  14337  efgi2  15036  fiinopn  16649  tgcl  16709  distop  16735  isclo2  16827  iscldtop  16834  ssnei2  16855  opnnei  16859  pnfnei  16952  mnfnei  16953  tgcnp  16985  cnpnei  16995  2ndcctbss  17183  1stcelcls  17189  txcnpi  17304  cnmptcom  17374  fbfinnfr  17538  isfildlem  17554  snfil  17561  fbunfip  17566  fgcl  17575  elfm2  17645  fmfnfmlem1  17651  fmco  17658  fbflim2  17674  flffbas  17692  cnpflf2  17697  flimfcls  17723  tmdgsum  17780  neibl  18049  metcnp3  18088  fgcfil  18699  caubl  18735  volsuplem  18914  ellimc3  19231  dvnadd  19280  dvnres  19282  cpnord  19286  dvnfre  19303  mpfrcl  19404  ply1divex  19524  aalioulem2  19715  cxpmul2  20038  wilthlem3  20310  lgsquad2lem2  20600  qabvexp  20777  gxnn0add  20943  gxnn0mul  20946  ismgm  20989  isexid2  20994  ipassi  21421  ubthlem2  21452  isch3  21823  shintcli  21910  shmodsi  21970  spansncvi  22233  pjjsi  22281  hoaddsub  22398  eigorthi  22419  pjss2coi  22746  pjnormssi  22750  pj3cor1i  22791  strb  22840  dmdmd  22882  mdsl0  22892  csmdsymi  22916  chrelat2i  22947  cvati  22948  mdsymlem3  22987  mdsymlem6  22990  sumdmdlem2  23001  dmdbr5ati  23004  cvmlift2lem1  23835  3ccased  24075  dedekind  24084  dfres3  24118  dfon2lem3  24143  rdgprc  24153  trpredmintr  24236  trpredrec  24243  wfr3g  24257  wfrlem12  24269  frr3g  24282  frrlem11  24295  sltval2  24312  axcontlem4  24597  cgrextend  24633  btwndiff  24652  btwnconn1lem12  24723  brsegle  24733  broutsideof2  24747  funray  24765  meran1  24852  waj-ax  24855  arg-ax  24857  wl-pm2.86i  24923  isunscov  25085  restidsing  25087  twsymr  25089  prj1b  25090  prj3  25091  fixpc  25105  domintrefc  25136  mapmapmap  25159  injsurinj  25160  cbcpcp  25173  prl  25178  prl2  25180  prjmapcp2  25181  dstr  25182  jidd  25203  midd  25204  int2pre  25248  ubpar  25272  inposet  25289  tolat  25297  toplat  25301  latdir  25306  ridlideq  25346  rzrlzreq  25347  resgcom  25362  grpodivone  25384  grpodivfo  25385  rltrran  25425  zerdivemp1  25447  muldisc  25492  svli2  25495  svs2  25498  truni1  25516  truni2  25517  truni3  25518  inttop2  25526  nsn  25541  intopcoaconlem3b  25549  intopcoaconc  25552  qusp  25553  intcont  25554  prcnt  25562  fisub  25565  cmptdst  25579  exopcopn  25583  prdnei  25584  limptlimpr2lem1  25585  limptlimpr2lem2  25586  islimrs  25591  islimrs3  25592  islimrs4  25593  bwt2  25603  iintlem1  25621  iint  25623  lvsovso  25637  supnuf  25640  claddrvr  25659  sigadd  25660  addcomv  25666  addcanrg  25678  negveudr  25680  subclrvd  25685  distsava  25700  intvconlem1  25714  hdrmp  25717  cmppfd  25756  domcmpd  25757  codcmpd  25758  cmpasso  25784  cmpida  25785  cmpidb  25786  cmpassoh  25812  homgrf  25813  imonclem  25824  cmpmon  25826  iepiclem  25834  isepic  25835  idfisf  25852  issrc  25878  propsrc  25879  partarelt1  25907  inttarcar  25912  fnctartar  25918  fnctartar2  25919  prismorcset2  25929  cmpmor  25986  setiscat  25990  lemindclsbu  26006  indcls2  26007  clscnc  26021  pgapspf2  26064  gltpntl  26083  lineval5a  26099  lineval6a  26100  isconcl5a  26112  isconcl5ab  26113  isconcl6a  26114  isibg2aa  26123  isib2g1a1  26127  isibg1a2  26128  isibg2a  26129  isibg1a3a  26133  isibg1spa  26134  isibg1a5a  26135  bsstr  26139  nbssntr  26140  sgplpte21d  26147  segline  26152  pxysxy  26153  lppotoslem  26154  lppotos  26155  xsyysx  26156  nbssntrs  26158  pdiveql  26179  abhp  26184  elicc3  26239  nn0prpwlem  26249  nn0prpw  26250  fnessref  26304  neibastop2lem  26320  filnetlem4  26341  fzmul  26454  fdc  26466  seqpo  26468  incsequz  26469  isismty  26536  ismtybndlem  26541  heibor1lem  26544  ghomco  26584  zerdivemp1x  26597  pridlc  26707  ceqsex3OLD  26737  nelss  26762  incssnn0  26797  fphpd  26910  jm2.19lem3  27095  setindtr  27128  dfac21  27175  islssfg2  27180  mpaaeu  27366  psgnunilem4  27431  pm14.24  27643  stoweidlem26  27786  hirstL-ax3  27871  rexsb  27957  rexrsb  27958  2reu1  27975  afvres  28045  tz6.12-afv  28046  afvco2  28048  ndmaovdistr  28078  mpt2xopoveqd  28098  usgraeq12d  28122  usgraedgprv  28133  usgraedgrnv  28134  usgranloop  28135  usgra1v  28137  nbgraop  28151  nbusgra  28154  nbgranself2  28162  nbcusgra  28170  uvtxnbgra  28176  frgra2v  28188  frgra3vlem1  28189  frgra3vlem2  28190  3vfriswmgralem  28193  3vfriswmgra  28194  ad5ant23  28288  ad5ant24  28289  ad5ant25  28290  ad5ant245  28291  ad5ant234  28292  ad5ant235  28293  sb5ALT  28344  truniALT  28361  onfrALTlem3  28365  ee223  28468  eel12131  28555  eel32131  28558  3imp231  28664  3orbi123VD  28699  sbc3orgVD  28700  exbirVD  28702  exbiriVD  28703  sbcim2gVD  28724  trsbcVD  28726  truniALTVD  28727  onfrALTlem3VD  28736  onfrALTlem2VD  28738  csbrngVD  28745  19.41rgVD  28751  a9e2eqVD  28756  a9e2ndeqVD  28758  2uasbanhVD  28760  sb5ALTVD  28762  vk15.4jVD  28763  ax12-3  29177  ax9lem2  29214  ax9lem5  29217  ax9lem15  29227  ax9vax9  29231  cdleme18d  30557  tendovalco  31027  cdlemn11pre  31473  dihord2pre  31488
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator