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  368  pm2.62  395  impcom  415  imp3a  416  expcom  420  exp3a  421  pm3.21  428  imdistanri  663  pm2.64  721  pm2.75  779  ccased  872  dedlem0b  878  3impd  1121  3expd  1124  mp3an1i  1225  simplbi2com  1306  meredith  1310  ax12olem21  1550  ax12olem23  1552  ax10lem16  1560  ax10  1572  hbimd  1665  19.21t  1668  equtrr  1686  sbequ2  1740  ax11b  1786  sb6rf  1828  sb56  1834  exmoeu  1988  moimv  1994  eupickbi  2012  2eu1  2026  exists2  2036  r19.12  2375  2gencl  2500  3gencl  2501  rcla4cv  2555  ceqex  2570  mob  2627  euind  2632  reuind  2646  sseq2  2833  uneqdifeq  3154  difsn  3359  eqsn  3375  preq12b  3386  intab  3484  iinss2  3545  trint0  3686  dtru  3754  sspwb  3774  copsexg  3802  pocl  3868  pofun  3877  solin  3884  frss  3907  tz7.7  3965  ordtri3  3975  ordtr2  3983  suc11  4041  onssneli  4047  eusv2  4091  ralxfrALT  4115  iunpw  4133  ordom  4228  limom  4234  peano5  4242  2optocl  4344  3optocl  4345  ssrel  4355  ssrelrel  4365  relop  4412  xpidtr  4641  trin2  4642  sotri3  4649  poltletr  4654  xp11  4687  relcnvtr  4767  funmo  4796  fss  4920  fv3  5054  tz6.12-1  5057  tz6.12c  5061  tz6.12i  5062  mpteqb  5123  fornex  5192  funfvima  5258  fvclss  5265  f1fveq  5290  isotr  5330  isotrALT  5331  isoselem  5336  oprabid  5377  ovg  5474  poxp  5704  soxp  5705  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  5983  oaordex  6003  oalimcl  6005  oaass  6006  omordi  6011  omlimcl  6023  odi  6024  omeulem1  6027  oen0  6031  oewordri  6037  nnawordi  6066  nnaass  6067  nnmordi  6076  omabs  6092  omsmolem  6098  iiner  6178  2ecoptocl  6186  3ecoptocl  6187  th3qlem2  6202  undifixp  6282  xpdom2  6386  xpf1o  6499  infensuc  6515  php  6521  onomeneq  6526  isinf  6549  findcard2  6571  unblem2  6583  finsschain  6634  marypha1  6659  supub  6680  suplub  6681  supsnALT  6696  hartogs  6732  card2on  6741  card2inf  6742  xpwdomg  6772  elirrv  6784  inf3lem1  6802  inf3lem2  6803  inf3lem3  6804  inf3lem5  6806  noinfep  6833  noinfepOLD  6834  trcl  6883  en3lp  6891  tcel  6903  r1sdom  6919  rankonidlem  6972  rankxpsuc  7024  scottex  7027  pr2ne  7107  dif1card  7110  fodomnum  7156  cardaleph  7188  cflim2  7342  cfsmolem  7349  infpssrlem3  7384  isfin7-2  7475  fin1a2lem6  7484  fin1a2lem10  7488  fin1a2lem12  7490  domtriomlem  7521  axdc3lem4  7532  axdc4lem  7534  kmlem4  7572  kmlem9  7577  kmlem12  7580  kmlem13  7581  zorn2lem3  7591  zorn2lem4  7592  zorn2lem5  7593  zorn2lem6  7594  zorn2lem7  7595  zornn0g  7598  axdclem  7612  axdclem2  7613  ondomon  7649  alephval2  7656  cfpwsdom  7668  axrepnd  7678  tskr1om  7802  grupr  7830  gruiun  7832  ingru  7847  grothomex  7861  indpi  7941  nqereu  7963  genpnnp  8039  prlem934  8067  ltaddpr2  8069  reclem2pr  8082  mulgt0sr  8137  supsrlem  8143  mul0ori  8622  lemul1a  8762  squeeze0  8826  peano5nni  8875  nnunb  9062  fzind  9202  nn0ind-raph  9205  zindd  9206  eluzadd  9340  uzin  9344  xmulasslem  9623  icoshft  9770  fzen  9821  expcllem  10099  expeq0  10117  mulexp  10126  expword2i  10143  bernneq  10209  facdiv  10239  hashmap  10324  cjexp  10420  absexp  10552  abssubne0  10570  iseraltlem2  10773  sin01gt0  11063  alzdvds  11170  dvdslegcd  11210  gcdneg  11219  rplpwr  11249  qredeq  11299  prmpwdvds  11434  prmreclem4  11449  ramcl  11559  imasleval  11905  drsdirfi  11958  spwmo  12199  efgi2  12897  mreiincl  14392  fiinopn  14481  tgcl  14541  distop  14567  isclo2  14658  iscldtop  14665  ssnei2  14686  opnnei  14690  pnfnei  14769  mnfnei  14770  tgcnp  14802  cnpnei  14812  2ndcctbss  14996  1stcelcls  15002  txcnpi  15117  cnmptcom  15187  fbfinnfr  15351  isfildlem  15367  snfil  15374  fbunfip  15379  fgcl  15388  elfm2  15458  fmfnfmlem1  15464  fmco  15471  fbflim2  15487  flffbas  15505  cnpflf2  15510  flimfcls  15536  tmdgsum  15593  xmeteq0  15718  neibl  15863  metcnp3  15902  fgcfil  16504  caubl  16540  volsuplem  16719  dvnadd  17061  dvnres  17062  cpnord  17066  mpfrcl  17154  ply1divex  17272  cxpmul2  17714  wilthlem3  17892  lgsquad2lem2  18073  qabvexp  18112  gxnn0add  18257  gxnn0mul  18260  ismgm  18303  isexid2  18308  rngodm1dm2  18401  ipassi  18735  ubthlem2  18766  isch3  19137  shintcli  19224  shmodsi  19284  spansncvi  19565  pjjsi  19613  hoaddsub  19712  eigorthi  19733  pjss2coi  20060  pjnormssi  20064  pj3cor1i  20105  strb  20154  dmdmd  20196  mdsl0  20206  csmdsymi  20230  chrelat2i  20261  cvati  20262  mdsymlem3  20301  mdsymlem6  20304  sumdmdlem2  20315  dmdbr5ati  20318  cvmlift2lem1  20490  3ccased  20748  dedekind  20753  dfres3  20788  dfon2lem3  20815  rdgprc  20825  trpredmintr  20909  trpredrec  20916  wfr3g  20930  wfrlem12  20942  frr3g  20955  frrlem11  20968  sltval2  20984  axfelem13  21033  elfuns  21135  axcontlem4  21276  cgrextend  21312  btwndiff  21331  btwnconn1lem12  21402  brsegle  21412  broutsideof2  21426  funray  21444  meran1  21506  waj-ax  21509  arg-ax  21511  wl-pm2.86i  21577  copsexgb  21610  evpexun  21639  isunscov  21691  restidsing  21693  twsymr  21695  prj1b  21696  prj3  21697  fixpc  21711  domintrefc  21743  mapmapmap  21768  injsurinj  21769  repfuntw  21780  cbcpcp  21782  prl  21787  prl2  21789  prjmapcp2  21790  dstr  21791  jidd  21812  midd  21813  int2pre  21857  ubpar  21881  inposet  21898  tolat  21906  toplat  21910  latdir  21915  ridlideq  21955  rzrlzreq  21956  resgcom  21971  grpodivone  21993  grpodivfo  21994  rltrran  22034  zerdivemp1  22056  zintdom  22058  muldisc  22104  svli2  22107  svs2  22110  truni1  22128  truni2  22129  truni3  22130  inttop2  22141  npmp  22147  nsn  22156  intopcoaconlem3b  22164  intopcoaconc  22167  qusp  22168  intcont  22169  prcnt  22177  fisub  22180  cmptdst  22194  exopcopn  22198  prdnei  22199  limptlimpr2lem1  22200  limptlimpr2lem2  22201  islimrs  22206  islimrs3  22207  islimrs4  22208  bwt2  22218  iintlem1  22236  iint  22238  lvsovso  22252  supnuf  22255  claddrvr  22274  sigadd  22275  addcomv  22281  addcanrg  22293  negveudr  22295  subclrvd  22300  distsava  22315  intvconlem1  22329  hdrmp  22332  cmppfd  22371  domcmpd  22372  codcmpd  22373  cmpasso  22399  cmpida  22400  cmpidb  22401  cmpassoh  22427  homgrf  22428  imonclem  22439  cmpmon  22441  iepiclem  22449  isepic  22450  idfisf  22467  issrc  22493  propsrc  22494  partarelt1  22522  inttaror  22526  inttarcar  22527  fnctartar  22533  fnctartar2  22534  prismorcset2  22544  cmpmor  22601  setiscat  22605  isconcl5  22636  isconcl6  22637  isibg2  22644  lemindclsbu  22682  indcls2  22683  clscnc  22697  pgapspf2  22740  elicc3  22772  nn0prpwlem  22782  nn0prpw  22783  fnessref  22837  neibastop2lem  22853  filnetlem4  22874  fzmul  22988  fdc  23000  seqpo  23002  incsequz  23003  isismty  23070  ismtybndlem  23075  heibor1lem  23078  ghomco  23118  zerdivemp1x  23131  pridlc  23241  ceqsex3OLD  23271  nelss  23296  incssnn0  23333  fphpd  23444  jm2.19lem3  23663  setindtr  23696  dfac21  23749  aalioulem2  23763  islssfg2  23793  mpaaeu  23979  psgnunilem4  24044  pm14.24  24287  hirstL-ax3  24340  sb5ALT  24430  truniALT  24447  onfrALTlem3  24451  ee223  24540  3orbi123VD  24703  sbc3orgVD  24704  exbirVD  24706  exbiriVD  24707  sbcim2gVD  24728  trsbcVD  24730  truniALTVD  24731  onfrALTlem3VD  24740  onfrALTlem2VD  24742  csbrngVD  24749  19.41rgVD  24755  a9e2eqVD  24760  a9e2ndeqVD  24762  2uasbanhVD  24764  sb5ALTVD  24766  vk15.4jVD  24767  ax12-3  26287  ax9lem2  26324  ax9lem5  26327  ax9lem15  26337  ax9vax9  26341  cdleme18d  27667  tendovalco  28137  cdlemn11pre  28583  dihord2pre  28598
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
Copyright terms: Public domain