HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
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  329  jaod  368  orel1  369  pm2.62  396  impcom  416  imp3a  417  expcom  421  exp3a  422  pm3.21  429  imdistanri  668  pm2.64  726  pm2.75  783  ccased  882  dedlem0b  888  3impd  1133  3expd  1136  mp3an1i  1237  simplbi2com  1318  meredith  1322  ax12olem21  1569  ax12olem23  1571  ax10lem16  1579  ax10  1591  hbimd  1686  19.21t  1689  equtrr  1707  sbequ2  1761  ax11b  1807  sb6rf  1849  sb56  1855  exmoeu  2009  moimv  2015  eupickbi  2033  2eu1  2047  exists2  2057  r19.12  2395  2gencl  2520  3gencl  2521  rcla4cv  2575  ceqex  2590  mob  2647  euind  2652  reuind  2666  sseq2  2853  uneqdifeq  3175  difsn  3377  eqsn  3393  preq12b  3404  intab  3502  iinss2  3563  trint0  3704  dtru  3772  sspwb  3792  copsexg  3820  pocl  3886  pofun  3895  solin  3902  frss  3925  tz7.7  3983  ordtri3  3993  ordtr2  4001  suc11  4059  onssneli  4065  eusv2  4109  ralxfrALT  4135  iunpw  4156  ordom  4251  limom  4257  peano5  4265  2optocl  4366  3optocl  4367  ssrel  4377  ssrelrel  4386  relop  4433  eliniseg2  4631  sotri3  4653  poltletr  4658  xp11  4691  relcnvtr  4771  funmo  4800  fss  4924  fv3  5058  tz6.12-1  5061  tz6.12c  5065  tz6.12i  5066  ndmfv  5070  mpteqb  5125  fornex  5194  funfvima  5260  fvclss  5266  f1fveq  5291  isotr  5331  isotrALT  5332  isoselem  5337  oprabid  5377  ovg  5474  poxp  5705  soxp  5706  tposfn2  5731  sorpsscmpl  5759  iotaval  5773  onnseq  5808  smores  5816  smoel  5824  smogt  5831  smoiso2  5833  tfrlem2  5839  tfr3  5862  tz7.48-2  5901  tz7.48-3  5903  tz7.49  5904  abianfp  5918  oecl  5980  oaordex  6000  oalimcl  6002  oaass  6003  omordi  6008  omlimcl  6020  odi  6021  omeulem1  6024  oen0  6028  oewordri  6034  nnawordi  6063  nnaass  6064  nnmordi  6073  omabs  6087  omsmolem  6093  xpidtr  6172  iiner  6174  2ecoptocl  6182  3ecoptocl  6183  th3qlem2  6198  undifixp  6277  xpdom2  6381  xpf1o  6494  infensuc  6510  php  6516  onomeneq  6521  isinf  6544  findcard2  6561  unblem2  6573  finsschain  6624  marypha1  6649  supub  6670  suplub  6671  supsnALT  6686  hartogs  6722  card2on  6731  card2inf  6732  xpwdomg  6762  elirrv  6774  inf3lem1  6792  inf3lem2  6793  inf3lem3  6794  inf3lem5  6796  noinfep  6823  noinfepOLD  6824  trcl  6873  en3lp  6881  tcel  6893  r1sdom  6909  rankonidlem  6962  rankxpsuc  7014  scottex  7017  pr2ne  7097  dif1card  7100  fodomnum  7146  cardaleph  7178  cflim2  7332  cfsmolem  7339  infpssrlem3  7374  isfin7-2  7465  fin1a2lem6  7474  fin1a2lem10  7478  fin1a2lem12  7480  domtriomlem  7511  axdc3lem4  7522  axdc4lem  7524  kmlem4  7562  kmlem9  7567  kmlem12  7570  kmlem13  7571  zorn2lem3  7581  zorn2lem4  7582  zorn2lem5  7583  zorn2lem6  7584  zorn2lem7  7585  zornn0g  7588  axdclem  7602  axdclem2  7603  ondomon  7639  alephval2  7646  cfpwsdom  7658  axrepnd  7668  tskr1om  7792  grupr  7820  gruiun  7822  ingru  7837  grothomex  7851  indpi  7931  nqereu  7953  genpnnp  8029  prlem934  8057  ltaddpr2  8059  reclem2pr  8072  mulgt0sr  8127  supsrlem  8133  mul0ori  8612  lemul1a  8752  squeeze0  8816  peano5nni  8865  nnunb  9052  fzind  9192  nn0ind-raph  9195  zindd  9196  eluzadd  9330  uzin  9334  xmulasslem  9610  icoshft  9757  fzen  9808  expcllem  10085  expeq0  10103  mulexp  10112  expword2i  10129  bernneq  10194  facdiv  10224  hashmap  10296  cjexp  10392  absexp  10524  abssubne0  10542  iseraltlem2  10745  sin01gt0  11035  alzdvds  11142  dvdslegcd  11182  gcdneg  11191  rplpwr  11221  qredeq  11271  prmpwdvds  11406  prmreclem4  11421  ramcl  11531  imasleval  11871  drsdirfi  11924  trin2  12155  spwmo  12169  efgi2  12793  mreiincl  14301  fiinopn  14390  tgcl  14450  distop  14476  isclo2  14567  iscldtop  14574  ssnei2  14595  opnnei  14599  pnfnei  14678  mnfnei  14679  tgcnp  14711  cnpnei  14721  2ndcctbss  14905  1stcelcls  14911  txcnpi  15026  cnmptcom  15096  fbfinnfr  15260  isfildlem  15276  snfil  15283  fbunfip  15288  fgcl  15297  elfm2  15367  fmfnfmlem1  15373  fmco  15380  fbflim2  15396  flffbas  15414  cnpflf2  15419  flimfcls  15445  tmdgsum  15502  xmeteq0  15627  neibl  15772  metcnp3  15811  nmvs  15912  fgcfil  16413  caubl  16449  volsuplem  16628  dvnadd  16970  dvnres  16971  cpnord  16975  mpfrcl  17063  ply1divex  17181  cxpmul2  17623  wilthlem3  17801  lgsquad2lem2  17982  qabvexp  18021  gxnn0add  18162  gxnn0mul  18165  ismgm  18208  isexid2  18213  rngodm1dm2  18306  ipassi  18640  ubthlem2  18671  isch3  19042  shintcli  19129  shmodsi  19189  spansncvi  19470  pjjsi  19518  hoaddsub  19617  eigorthi  19638  pjss2coi  19965  pjnormssi  19969  pj3cor1i  20010  strb  20059  dmdmd  20101  mdsl0  20111  csmdsymi  20135  chrelat2i  20166  cvati  20167  mdsymlem3  20206  mdsymlem6  20209  sumdmdlem2  20220  dmdbr5ati  20223  cvmlift2lem1  20400  3ccased  20663  dedekind  20669  dfres3  20704  dfon2lem3  20731  rdgprc  20742  trpredmintr  20827  trpredrec  20834  wfr3g  20848  wfrlem12  20860  frr3g  20873  frrlem11  20886  sltval2  20902  axfelem13  20951  elfuns  21053  axcontlem4  21194  cgrextend  21230  btwndiff  21249  btwnconn1lem12  21320  brsegle  21330  broutsideof2  21344  funray  21362  meran1  21424  waj-ax  21427  arg-ax  21429  wl-pm2.86i  21495  copsexgb  21530  evpexun  21559  isunscov  21613  restidsing  21615  twsymr  21617  prj1b  21618  prj3  21619  fixpc  21635  domintrefc  21667  mapmapmap  21692  injsurinj  21693  repfuntw  21705  cbcpcp  21707  prl  21712  prl2  21714  prjmapcp2  21715  dstr  21716  jidd  21737  midd  21738  int2pre  21782  ubpar  21806  inposet  21823  tolat  21831  toplat  21835  latdir  21840  ridlideq  21880  rzrlzreq  21881  resgcom  21896  grpodivone  21918  grpodivfo  21919  rltrran  21959  zerdivemp1  21981  zintdom  21983  muldisc  22029  svli2  22032  svs2  22035  truni1  22053  truni2  22054  truni3  22055  inttop2  22066  npmp  22072  nsn  22081  intopcoaconlem3b  22089  intopcoaconc  22092  qusp  22093  intcont  22094  prcnt  22102  efilcp  22103  fisub  22105  cmptdst  22119  exopcopn  22123  prdnei  22124  limptlimpr2lem1  22125  limptlimpr2lem2  22126  islimrs  22131  islimrs3  22132  islimrs4  22133  bwt2  22143  iintlem1  22161  iint  22163  lvsovso  22177  supnuf  22180  claddrvr  22199  sigadd  22200  addcomv  22206  addcanrg  22218  negveudr  22220  subclrvd  22225  distsava  22240  intvconlem1  22256  hdrmp  22259  cmppfd  22298  domcmpd  22299  codcmpd  22300  cmpasso  22326  cmpida  22327  cmpidb  22328  cmpassoh  22354  homgrf  22355  imonclem  22366  cmpmon  22368  iepiclem  22376  isepic  22377  idfisf  22394  issrc  22420  propsrc  22421  partarelt1  22449  inttaror  22453  inttarcar  22454  fnctartar  22460  fnctartar2  22461  prismorcset2  22472  cmpmor  22529  setiscat  22533  lemindclsbu  22584  indcls2  22585  clscnc  22599  pgapspf2  22642  elicc3  22674  nn0prpwlem  22684  nn0prpw  22685  fnessref  22739  neibastop2lem  22755  filnetlem4  22776  fzmul  22891  fdc  22903  seqpo  22905  incsequz  22906  isismty  22973  ismtybndlem  22978  heibor1lem  22981  ghomco  23021  zerdivemp1x  23034  pridlc  23144  ceqsex3OLD  23174  nelss  23200  incssnn0  23237  fphpd  23348  jm2.19lem3  23567  setindtr  23600  dfac21  23653  aalioulem2  23667  islssfg2  23697  hbtlem5  23860  mpaaeu  23883  psgnunilem4  23948  pm14.24  24195  hirstL-ax3  24248  sb5ALT  24339  truniALT  24356  onfrALTlem3  24360  ee223  24449  3orbi123VD  24612  sbc3orgVD  24613  exbirVD  24615  exbiriVD  24616  sbcim2gVD  24637  trsbcVD  24639  truniALTVD  24640  onfrALTlem3VD  24649  onfrALTlem2VD  24651  csbrngVD  24658  19.41rgVD  24664  a9e2eqVD  24669  a9e2ndeqVD  24671  2uasbanhVD  24673  sb5ALTVD  24675  vk15.4jVD  24676  ax12-3  26196  ax9lem2  26233  ax9lem5  26236  ax9lem15  26246  ax9vax9  26250  cdleme18d  27577  tendovalco  28047  cdlemn11pre  28493  dihord2pre  28508
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
Copyright terms: Public domain