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  328  jaod  367  orel1  369  pm2.62  396  impcom  416  imp3a  417  expcom  421  exp3a  422  pm3.21  429  imdistanri  665  pm2.64  724  pm2.75  782  ccased  875  dedlem0b  881  3impd  1124  3expd  1127  mp3an1i  1228  simplbi2com  1309  meredith  1313  ax12olem21  1554  ax12olem23  1556  ax10lem16  1564  ax10lem26  1574  ax10  1576  hbimd  1669  19.21t  1672  equtrr  1690  sbequ2  1744  ax11b  1790  sb6rf  1832  sb56  1838  exmoeu  1992  moimv  1998  eupickbi  2016  2eu1  2030  exists2  2040  r19.12  2379  2gencl  2504  3gencl  2505  rcla4cv  2559  ceqex  2574  mob  2631  euind  2636  reuind  2650  sseq2  2837  uneqdifeq  3159  difsn  3364  eqsn  3382  preq12b  3395  intab  3494  iinss2  3555  trint0  3696  dtru  3764  sspwb  3784  copsexg  3812  pocl  3878  pofun  3887  solin  3894  frss  3917  tz7.7  3975  ordtri3  3985  ordtr2  3993  suc11  4051  onssneli  4057  eusv2  4101  ralxfrALT  4125  iunpw  4143  ordom  4238  limom  4244  peano5  4252  2optocl  4354  3optocl  4355  ssrel  4365  ssrelrel  4375  relop  4422  xpidtr  4652  trin2  4653  sotri3  4660  poltletr  4665  xp11  4698  relcnvtr  4778  funmo  4807  fss  4931  fv3  5066  tz6.12-1  5069  tz6.12c  5073  tz6.12i  5074  mpteqb  5136  fornex  5205  funfvima  5271  fvclss  5278  f1fveq  5303  isotr  5343  isotrALT  5344  isoselem  5349  oprabid  5390  ovg  5487  poxp  5718  soxp  5719  tposfn2  5745  sorpsscmpl  5773  iotaval  5787  onnseq  5822  smores  5830  smoel  5838  smogt  5845  smoiso2  5847  tfrlem2  5853  tfr3  5876  tz7.48-2  5915  tz7.48-3  5917  tz7.49  5918  abianfp  5932  oecl  5997  oaordex  6017  oalimcl  6019  oaass  6020  omordi  6025  omlimcl  6037  odi  6038  omeulem1  6041  oen0  6045  oewordri  6051  nnawordi  6080  nnaass  6081  nnmordi  6090  omabs  6106  omsmolem  6112  iiner  6192  2ecoptocl  6200  3ecoptocl  6201  th3qlem2  6216  undifixp  6296  xpdom2  6400  xpf1o  6513  infensuc  6529  php  6535  onomeneq  6540  isinf  6565  findcard2  6587  unblem2  6599  finsschain  6650  marypha1  6675  supub  6696  suplub  6697  supsnALT  6712  hartogs  6748  card2on  6757  card2inf  6758  xpwdomg  6788  elirrv  6800  inf3lem1  6818  inf3lem2  6819  inf3lem3  6820  inf3lem5  6822  noinfep  6849  noinfepOLD  6850  trcl  6899  en3lp  6907  tcel  6919  r1sdom  6935  rankonidlem  6988  rankxpsuc  7040  scottex  7043  pr2ne  7123  dif1card  7126  fodomnum  7172  cardaleph  7204  cflim2  7358  cfsmolem  7365  infpssrlem3  7400  isfin7-2  7491  fin1a2lem6  7500  fin1a2lem10  7504  fin1a2lem12  7506  domtriomlem  7537  axdc3lem4  7548  axdc4lem  7550  kmlem4  7588  kmlem9  7593  kmlem12  7596  kmlem13  7597  zorn2lem3  7607  zorn2lem4  7608  zorn2lem5  7609  zorn2lem6  7610  zorn2lem7  7611  zornn0g  7614  axdclem  7628  axdclem2  7629  ondomon  7665  alephval2  7672  cfpwsdom  7684  axrepnd  7694  tskr1om  7819  grupr  7847  gruiun  7849  ingru  7864  grothomex  7878  indpi  7958  nqereu  7980  genpnnp  8056  prlem934  8084  ltaddpr2  8086  reclem2pr  8099  mulgt0sr  8154  supsrlem  8160  lemul1a  8998  squeeze0  9047  peano5nni  9136  nnunb  9345  fzind  9493  nn0ind-raph  9496  zindd  9497  eluzadd  9640  uzin  9644  xmulasslem  9988  icoshft  10138  fzen  10189  expcllem  10484  expeq0  10502  mulexp  10511  leexp2r  10529  bernneq  10596  facdiv  10669  hashmap  10755  cjexp  10845  absexp  10997  iseraltlem2  11362  sin01gt0  11669  alzdvds  11776  dvdslegcd  11816  gcdneg  11826  rplpwr  11856  qredeq  11906  prmpwdvds  12072  prmreclem4  12087  ramcl  12197  imasleval  12544  mreiincl  12597  drsdirfi  12649  spwmo  12903  efgi2  13760  fiinopn  15370  tgcl  15430  distop  15456  isclo2  15547  iscldtop  15554  ssnei2  15575  opnnei  15579  pnfnei  15658  mnfnei  15659  tgcnp  15691  cnpnei  15701  2ndcctbss  15885  1stcelcls  15891  txcnpi  16006  cnmptcom  16076  fbfinnfr  16240  isfildlem  16256  snfil  16263  fbunfip  16268  fgcl  16277  elfm2  16347  fmfnfmlem1  16353  fmco  16360  fbflim2  16376  flffbas  16394  cnpflf2  16399  flimfcls  16425  tmdgsum  16482  xmeteq0  16607  neibl  16752  metcnp3  16791  fgcfil  17394  caubl  17430  volsuplem  17609  dvnadd  17951  dvnres  17952  cpnord  17956  mpfrcl  18064  ply1divex  18182  cxpmul2  18643  wilthlem3  18879  lgsquad2lem2  19169  qabvexp  19346  gxnn0add  19493  gxnn0mul  19496  ismgm  19539  isexid2  19544  rngodm1dm2  19637  ipassi  19971  ubthlem2  20002  isch3  20373  shintcli  20460  shmodsi  20520  spansncvi  20801  pjjsi  20849  hoaddsub  20948  eigorthi  20969  pjss2coi  21296  pjnormssi  21300  pj3cor1i  21341  strb  21390  dmdmd  21432  mdsl0  21442  csmdsymi  21466  chrelat2i  21497  cvati  21498  mdsymlem3  21537  mdsymlem6  21540  sumdmdlem2  21551  dmdbr5ati  21554  cvmlift2lem1  21726  3ccased  21969  dedekind  21973  dfres3  22005  dfon2lem3  22028  rdgprc  22038  trpredmintr  22122  trpredrec  22129  wfr3g  22143  wfrlem12  22155  frr3g  22168  frrlem11  22181  sltval2  22197  axfelem13  22246  elfuns  22348  axcontlem4  22489  cgrextend  22525  btwndiff  22544  btwnconn1lem12  22615  brsegle  22625  broutsideof2  22639  funray  22657  meran1  22719  waj-ax  22722  arg-ax  22724  wl-pm2.86i  22790  copsexgb  22825  evpexun  22854  isunscov  22906  restidsing  22908  twsymr  22910  prj1b  22911  prj3  22912  fixpc  22926  domintrefc  22958  mapmapmap  22982  injsurinj  22983  repfuntw  22994  cbcpcp  22996  prl  23001  prl2  23003  prjmapcp2  23004  dstr  23005  jidd  23026  midd  23027  int2pre  23071  ubpar  23095  inposet  23112  tolat  23120  toplat  23124  latdir  23129  ridlideq  23169  rzrlzreq  23170  resgcom  23185  grpodivone  23207  grpodivfo  23208  rltrran  23248  zerdivemp1  23270  zintdom  23272  muldisc  23318  svli2  23321  svs2  23324  truni1  23342  truni2  23343  truni3  23344  inttop2  23355  npmp  23361  nsn  23370  intopcoaconlem3b  23378  intopcoaconc  23381  qusp  23382  intcont  23383  prcnt  23391  fisub  23394  cmptdst  23408  exopcopn  23412  prdnei  23413  limptlimpr2lem1  23414  limptlimpr2lem2  23415  islimrs  23420  islimrs3  23421  islimrs4  23422  bwt2  23432  iintlem1  23450  iint  23452  lvsovso  23466  supnuf  23469  claddrvr  23488  sigadd  23489  addcomv  23495  addcanrg  23507  negveudr  23509  subclrvd  23514  distsava  23529  intvconlem1  23543  hdrmp  23546  cmppfd  23585  domcmpd  23586  codcmpd  23587  cmpasso  23613  cmpida  23614  cmpidb  23615  cmpassoh  23641  homgrf  23642  imonclem  23653  cmpmon  23655  iepiclem  23663  isepic  23664  idfisf  23681  issrc  23707  propsrc  23708  partarelt1  23736  inttaror  23740  inttarcar  23741  fnctartar  23747  fnctartar2  23748  prismorcset2  23758  cmpmor  23815  setiscat  23819  lemindclsbu  23833  indcls2  23834  clscnc  23848  pgapspf2  23891  lineval5a  23921  lineval6a  23922  isconcl5a  23935  isconcl6a  23936  isibg1a1  23945  isibg1a2  23946  isibg2a  23947  isibg1a3a  23948  isibg1a4a  23949  isibg1a5a  23950  sgplpte21d  23960  elicc3  24019  nn0prpwlem  24029  nn0prpw  24030  fnessref  24084  neibastop2lem  24100  filnetlem4  24121  fzmul  24235  fdc  24247  seqpo  24249  incsequz  24250  isismty  24317  ismtybndlem  24322  heibor1lem  24325  ghomco  24365  zerdivemp1x  24378  pridlc  24488  ceqsex3OLD  24518  nelss  24543  incssnn0  24580  fphpd  24690  jm2.19lem3  24875  setindtr  24908  dfac21  24959  aalioulem2  24973  islssfg2  25003  mpaaeu  25189  psgnunilem4  25254  pm14.24  25470  hirstL-ax3  25523  sb5ALT  25621  truniALT  25638  onfrALTlem3  25642  ee223  25731  3orbi123VD  25894  sbc3orgVD  25895  exbirVD  25897  exbiriVD  25898  sbcim2gVD  25919  trsbcVD  25921  truniALTVD  25922  onfrALTlem3VD  25931  onfrALTlem2VD  25933  csbrngVD  25940  19.41rgVD  25946  a9e2eqVD  25951  a9e2ndeqVD  25953  2uasbanhVD  25955  sb5ALTVD  25957  vk15.4jVD  25958  ax12-3  27474  ax9lem2  27511  ax9lem5  27514  ax9lem15  27524  ax9vax9  27528  cdleme18d  28854  tendovalco  29324  cdlemn11pre  29770  dihord2pre  29785
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
Copyright terms: Public domain