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  664  pm2.64  722  pm2.75  780  ccased  873  dedlem0b  879  3impd  1122  3expd  1125  mp3an1i  1226  simplbi2com  1307  meredith  1311  ax12olem21  1551  ax12olem23  1553  ax10lem16  1561  ax10  1573  hbimd  1666  19.21t  1669  equtrr  1687  sbequ2  1741  ax11b  1787  sb6rf  1829  sb56  1835  exmoeu  1989  moimv  1995  eupickbi  2013  2eu1  2027  exists2  2037  r19.12  2376  2gencl  2501  3gencl  2502  rcla4cv  2556  ceqex  2571  mob  2628  euind  2633  reuind  2647  sseq2  2834  uneqdifeq  3156  difsn  3361  eqsn  3377  preq12b  3388  intab  3486  iinss2  3547  trint0  3688  dtru  3756  sspwb  3776  copsexg  3804  pocl  3870  pofun  3879  solin  3886  frss  3909  tz7.7  3967  ordtri3  3977  ordtr2  3985  suc11  4043  onssneli  4049  eusv2  4093  ralxfrALT  4117  iunpw  4135  ordom  4230  limom  4236  peano5  4244  2optocl  4346  3optocl  4347  ssrel  4357  ssrelrel  4367  relop  4414  xpidtr  4644  trin2  4645  sotri3  4652  poltletr  4657  xp11  4690  relcnvtr  4770  funmo  4799  fss  4923  fv3  5057  tz6.12-1  5060  tz6.12c  5064  tz6.12i  5065  mpteqb  5126  fornex  5195  funfvima  5261  fvclss  5268  f1fveq  5293  isotr  5333  isotrALT  5334  isoselem  5339  oprabid  5380  ovg  5477  poxp  5708  soxp  5709  tposfn2  5735  sorpsscmpl  5763  iotaval  5777  onnseq  5812  smores  5820  smoel  5828  smogt  5835  smoiso2  5837  tfrlem2  5843  tfr3  5866  tz7.48-2  5905  tz7.48-3  5907  tz7.49  5908  abianfp  5922  oecl  5987  oaordex  6007  oalimcl  6009  oaass  6010  omordi  6015  omlimcl  6027  odi  6028  omeulem1  6031  oen0  6035  oewordri  6041  nnawordi  6070  nnaass  6071  nnmordi  6080  omabs  6096  omsmolem  6102  iiner  6182  2ecoptocl  6190  3ecoptocl  6191  th3qlem2  6206  undifixp  6286  xpdom2  6390  xpf1o  6503  infensuc  6519  php  6525  onomeneq  6530  isinf  6555  findcard2  6577  unblem2  6589  finsschain  6640  marypha1  6665  supub  6686  suplub  6687  supsnALT  6702  hartogs  6738  card2on  6747  card2inf  6748  xpwdomg  6778  elirrv  6790  inf3lem1  6808  inf3lem2  6809  inf3lem3  6810  inf3lem5  6812  noinfep  6839  noinfepOLD  6840  trcl  6889  en3lp  6897  tcel  6909  r1sdom  6925  rankonidlem  6978  rankxpsuc  7030  scottex  7033  pr2ne  7113  dif1card  7116  fodomnum  7162  cardaleph  7194  cflim2  7348  cfsmolem  7355  infpssrlem3  7390  isfin7-2  7481  fin1a2lem6  7490  fin1a2lem10  7494  fin1a2lem12  7496  domtriomlem  7527  axdc3lem4  7538  axdc4lem  7540  kmlem4  7578  kmlem9  7583  kmlem12  7586  kmlem13  7587  zorn2lem3  7597  zorn2lem4  7598  zorn2lem5  7599  zorn2lem6  7600  zorn2lem7  7601  zornn0g  7604  axdclem  7618  axdclem2  7619  ondomon  7655  alephval2  7662  cfpwsdom  7674  axrepnd  7684  tskr1om  7808  grupr  7836  gruiun  7838  ingru  7853  grothomex  7867  indpi  7947  nqereu  7969  genpnnp  8045  prlem934  8073  ltaddpr2  8075  reclem2pr  8088  mulgt0sr  8143  supsrlem  8149  mul0ori  8631  lemul1a  8772  squeeze0  8836  peano5nni  8885  nnunb  9072  fzind  9213  nn0ind-raph  9216  zindd  9217  eluzadd  9351  uzin  9355  xmulasslem  9634  icoshft  9781  fzen  9832  expcllem  10121  expeq0  10139  mulexp  10148  expword2i  10166  bernneq  10233  facdiv  10263  hashmap  10349  cjexp  10445  absexp  10578  abssubne0  10596  iseraltlem2  10826  sin01gt0  11122  alzdvds  11229  dvdslegcd  11269  gcdneg  11278  rplpwr  11308  qredeq  11358  prmpwdvds  11522  prmreclem4  11537  ramcl  11647  imasleval  11993  mreiincl  12046  drsdirfi  12098  spwmo  12352  efgi2  13209  fiinopn  14816  tgcl  14876  distop  14902  isclo2  14993  iscldtop  15000  ssnei2  15021  opnnei  15025  pnfnei  15104  mnfnei  15105  tgcnp  15137  cnpnei  15147  2ndcctbss  15331  1stcelcls  15337  txcnpi  15452  cnmptcom  15522  fbfinnfr  15686  isfildlem  15702  snfil  15709  fbunfip  15714  fgcl  15723  elfm2  15793  fmfnfmlem1  15799  fmco  15806  fbflim2  15822  flffbas  15840  cnpflf2  15845  flimfcls  15871  tmdgsum  15928  xmeteq0  16053  neibl  16198  metcnp3  16237  fgcfil  16839  caubl  16875  volsuplem  17054  dvnadd  17396  dvnres  17397  cpnord  17401  mpfrcl  17490  ply1divex  17608  cxpmul2  18054  wilthlem3  18256  lgsquad2lem2  18532  qabvexp  18619  gxnn0add  18764  gxnn0mul  18767  ismgm  18810  isexid2  18815  rngodm1dm2  18908  ipassi  19242  ubthlem2  19273  isch3  19644  shintcli  19731  shmodsi  19791  spansncvi  20072  pjjsi  20120  hoaddsub  20219  eigorthi  20240  pjss2coi  20567  pjnormssi  20571  pj3cor1i  20612  strb  20661  dmdmd  20703  mdsl0  20713  csmdsymi  20737  chrelat2i  20768  cvati  20769  mdsymlem3  20808  mdsymlem6  20811  sumdmdlem2  20822  dmdbr5ati  20825  cvmlift2lem1  20997  3ccased  21242  dedekind  21247  dfres3  21279  dfon2lem3  21303  rdgprc  21313  trpredmintr  21397  trpredrec  21404  wfr3g  21418  wfrlem12  21430  frr3g  21443  frrlem11  21456  sltval2  21472  axfelem13  21521  elfuns  21623  axcontlem4  21764  cgrextend  21800  btwndiff  21819  btwnconn1lem12  21890  brsegle  21900  broutsideof2  21914  funray  21932  meran1  21994  waj-ax  21997  arg-ax  21999  wl-pm2.86i  22065  copsexgb  22100  evpexun  22129  isunscov  22181  restidsing  22183  twsymr  22185  prj1b  22186  prj3  22187  fixpc  22201  domintrefc  22233  mapmapmap  22257  injsurinj  22258  repfuntw  22269  cbcpcp  22271  prl  22276  prl2  22278  prjmapcp2  22279  dstr  22280  jidd  22301  midd  22302  int2pre  22346  ubpar  22370  inposet  22387  tolat  22395  toplat  22399  latdir  22404  ridlideq  22444  rzrlzreq  22445  resgcom  22460  grpodivone  22482  grpodivfo  22483  rltrran  22523  zerdivemp1  22545  zintdom  22547  muldisc  22593  svli2  22596  svs2  22599  truni1  22617  truni2  22618  truni3  22619  inttop2  22630  npmp  22636  nsn  22645  intopcoaconlem3b  22653  intopcoaconc  22656  qusp  22657  intcont  22658  prcnt  22666  fisub  22669  cmptdst  22683  exopcopn  22687  prdnei  22688  limptlimpr2lem1  22689  limptlimpr2lem2  22690  islimrs  22695  islimrs3  22696  islimrs4  22697  bwt2  22707  iintlem1  22725  iint  22727  lvsovso  22741  supnuf  22744  claddrvr  22763  sigadd  22764  addcomv  22770  addcanrg  22782  negveudr  22784  subclrvd  22789  distsava  22804  intvconlem1  22818  hdrmp  22821  cmppfd  22860  domcmpd  22861  codcmpd  22862  cmpasso  22888  cmpida  22889  cmpidb  22890  cmpassoh  22916  homgrf  22917  imonclem  22928  cmpmon  22930  iepiclem  22938  isepic  22939  idfisf  22956  issrc  22982  propsrc  22983  partarelt1  23011  inttaror  23015  inttarcar  23016  fnctartar  23022  fnctartar2  23023  prismorcset2  23033  cmpmor  23090  setiscat  23094  lemindclsbu  23108  indcls2  23109  clscnc  23123  pgapspf2  23166  lineval5a  23196  lineval6a  23197  isconcl5a  23210  isconcl6a  23211  isibg1a1  23220  isibg1a2  23221  isibg2a  23222  isibg1a3a  23223  isibg1a4a  23224  isibg1a5a  23225  sgplpte21d  23235  elicc3  23294  nn0prpwlem  23304  nn0prpw  23305  fnessref  23359  neibastop2lem  23375  filnetlem4  23396  fzmul  23510  fdc  23522  seqpo  23524  incsequz  23525  isismty  23592  ismtybndlem  23597  heibor1lem  23600  ghomco  23640  zerdivemp1x  23653  pridlc  23763  ceqsex3OLD  23793  nelss  23818  incssnn0  23855  fphpd  23966  jm2.19lem3  24151  setindtr  24184  dfac21  24235  aalioulem2  24249  islssfg2  24279  mpaaeu  24465  psgnunilem4  24530  pm14.24  24747  hirstL-ax3  24800  sb5ALT  24890  truniALT  24907  onfrALTlem3  24911  ee223  25000  3orbi123VD  25163  sbc3orgVD  25164  exbirVD  25166  exbiriVD  25167  sbcim2gVD  25188  trsbcVD  25190  truniALTVD  25191  onfrALTlem3VD  25200  onfrALTlem2VD  25202  csbrngVD  25209  19.41rgVD  25215  a9e2eqVD  25220  a9e2ndeqVD  25222  2uasbanhVD  25224  sb5ALTVD  25226  vk15.4jVD  25227  ax12-3  26747  ax9lem2  26784  ax9lem5  26787  ax9lem15  26797  ax9vax9  26801  cdleme18d  28127  tendovalco  28597  cdlemn11pre  29043  dihord2pre  29058
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
Copyright terms: Public domain