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  1640  equtrr  1672  ax12olem1  1880  ax12olem3  1882  ax10lem4  1894  ax11b  1948  sb6rf  2044  sb56  2050  exsb  2082  mo  2178  exmoeu  2198  morimv  2204  eupickbi  2222  2mo  2234  2eu1  2236  exists2  2246  r19.12  2669  2gencl  2830  3gencl  2831  rspccv  2894  ceqex  2911  mob  2960  euind  2965  reuind  2981  2rmorex  2982  sseq2  3213  reupick2  3467  uneqdifeq  3555  difsn  3768  eqsn  3791  preq12b  3804  iinss2  3970  disjxiun  4036  trint0  4146  dtru  4217  sspwb  4239  copsexg  4268  pocl  4337  pofun  4346  solin  4353  frss  4376  tz7.7  4434  ordtri3  4444  ordtr2  4452  suc11  4512  onssneli  4518  reusv1  4550  reusv2lem1  4551  alxfr  4563  ralxfrALT  4569  iunpw  4586  ordom  4681  limom  4687  peano5  4695  2optocl  4781  3optocl  4782  ssrel  4792  ssrelrel  4803  relop  4850  asymref2  5076  xpidtr  5081  trin2  5082  sotri3  5089  poltletr  5094  xp11  5127  relcnvtr  5208  iotaval  5246  funmo  5287  fss  5413  fv3  5557  tz6.12c  5563  tz6.12i  5564  mpteqb  5630  fornex  5766  funfvima  5769  fvclss  5776  f1fveq  5802  isoselem  5854  oprabid  5898  ovg  6002  poxp  6243  soxp  6244  tposfn2  6272  sorpsscmpl  6304  onnseq  6377  smoel  6393  smogt  6400  smoiso2  6402  tfrlem2  6408  tfr3  6431  tz7.48-2  6470  tz7.48-3  6472  tz7.49  6473  abianfp  6487  oecl  6552  oaordex  6572  oalimcl  6574  oaass  6575  omordi  6580  omlimcl  6592  odi  6593  omeulem1  6596  oen0  6600  oewordri  6606  nnawordi  6635  nnaass  6636  nnmordi  6645  omabs  6661  omsmolem  6667  iiner  6747  2ecoptocl  6765  3ecoptocl  6766  th3qlem2  6781  undifixp  6868  xpdom2  6973  xpf1o  7039  infensuc  7055  php  7061  onomeneq  7066  isinf  7092  findcard2  7114  unblem2  7126  finsschain  7178  marypha1  7203  hartogs  7275  card2on  7284  card2inf  7285  xpwdomg  7315  elirrv  7327  inf3lem1  7345  inf3lem2  7346  inf3lem3  7347  inf3lem5  7349  noinfep  7376  noinfepOLD  7377  trcl  7426  en3lp  7434  tcel  7446  r1sdom  7462  rankonidlem  7516  scottex  7571  pr2ne  7651  dif1card  7654  fodomnum  7700  cardaleph  7732  kmlem4  7795  kmlem9  7800  kmlem12  7803  kmlem13  7804  cflim2  7905  cfsmolem  7912  infpssrlem3  7947  isfin7-2  8038  fin1a2lem6  8047  fin1a2lem10  8051  fin1a2lem12  8053  domtriomlem  8084  axdc3lem4  8095  axdc4lem  8097  zorn2lem3  8141  zorn2lem4  8142  zorn2lem5  8143  zorn2lem6  8144  zorn2lem7  8145  zornn0g  8148  axdclem  8162  axdclem2  8163  ondomon  8201  alephval2  8210  cfpwsdom  8222  wunr1om  8357  wuncval2  8385  tskr1om  8405  grupr  8435  gruiun  8437  ingru  8453  grothomex  8467  indpi  8547  nqereu  8569  genpnnp  8645  prlem934  8673  ltaddpr2  8675  reclem2pr  8688  mulgt0sr  8743  supsrlem  8749  lemul1a  9626  squeeze0  9675  peano5nni  9765  nnunb  9977  fzind  10126  nn0ind-raph  10128  zindd  10129  eluzadd  10272  uzin  10276  xmulasslem  10621  icoshft  10774  fzen  10827  expcllem  11130  expeq0  11148  mulexp  11157  leexp2r  11175  bernneq  11243  facdiv  11316  hashmap  11403  cjexp  11651  absexp  11805  iseraltlem2  12171  sin01gt0  12486  alzdvds  12594  dvdslegcd  12711  gcdneg  12721  rplpwr  12751  qredeq  12801  prmpwdvds  12967  prmreclem4  12982  ramcl  13092  imasleval  13459  mreiincl  13514  mreexexd  13566  drsdirfi  14088  spwmo  14351  efgi2  15050  fiinopn  16663  tgcl  16723  distop  16749  isclo2  16841  iscldtop  16848  ssnei2  16869  opnnei  16873  pnfnei  16966  mnfnei  16967  tgcnp  16999  cnpnei  17009  2ndcctbss  17197  1stcelcls  17203  txcnpi  17318  cnmptcom  17388  fbfinnfr  17552  isfildlem  17568  snfil  17575  fbunfip  17580  fgcl  17589  elfm2  17659  fmfnfmlem1  17665  fmco  17672  fbflim2  17688  flffbas  17706  cnpflf2  17711  flimfcls  17737  tmdgsum  17794  neibl  18063  metcnp3  18102  fgcfil  18713  caubl  18749  volsuplem  18928  ellimc3  19245  dvnadd  19294  dvnres  19296  cpnord  19300  dvnfre  19317  mpfrcl  19418  ply1divex  19538  aalioulem2  19729  cxpmul2  20052  wilthlem3  20324  lgsquad2lem2  20614  qabvexp  20791  gxnn0add  20957  gxnn0mul  20960  ismgm  21003  isexid2  21008  ipassi  21435  ubthlem2  21466  isch3  21837  shintcli  21924  shmodsi  21984  spansncvi  22247  pjjsi  22295  hoaddsub  22412  eigorthi  22433  pjss2coi  22760  pjnormssi  22764  pj3cor1i  22805  strb  22854  dmdmd  22896  mdsl0  22906  csmdsymi  22930  chrelat2i  22961  cvati  22962  mdsymlem3  23001  mdsymlem6  23004  sumdmdlem2  23015  dmdbr5ati  23018  cvmlift2lem1  23848  3ccased  24088  dedekind  24097  prodmo  24159  dfres3  24187  dfon2lem3  24212  rdgprc  24222  trpredmintr  24305  trpredrec  24312  wfr3g  24326  wfrlem12  24338  frr3g  24351  frrlem11  24364  sltval2  24381  axcontlem4  24667  cgrextend  24703  btwndiff  24722  btwnconn1lem12  24793  brsegle  24803  broutsideof2  24817  funray  24835  meran1  24922  waj-ax  24925  arg-ax  24927  wl-pm2.86i  24993  isunscov  25177  restidsing  25179  twsymr  25181  prj1b  25182  prj3  25183  fixpc  25197  domintrefc  25228  mapmapmap  25251  injsurinj  25252  cbcpcp  25265  prl  25270  prl2  25272  prjmapcp2  25273  dstr  25274  jidd  25295  midd  25296  int2pre  25340  ubpar  25364  inposet  25381  tolat  25389  toplat  25393  latdir  25398  ridlideq  25438  rzrlzreq  25439  resgcom  25454  grpodivone  25476  grpodivfo  25477  rltrran  25517  zerdivemp1  25539  muldisc  25584  svli2  25587  svs2  25590  truni1  25608  truni2  25609  truni3  25610  inttop2  25618  nsn  25633  intopcoaconlem3b  25641  intopcoaconc  25644  qusp  25645  intcont  25646  prcnt  25654  fisub  25657  cmptdst  25671  exopcopn  25675  prdnei  25676  limptlimpr2lem1  25677  limptlimpr2lem2  25678  islimrs  25683  islimrs3  25684  islimrs4  25685  bwt2  25695  iintlem1  25713  iint  25715  lvsovso  25729  supnuf  25732  claddrvr  25751  sigadd  25752  addcomv  25758  addcanrg  25770  negveudr  25772  subclrvd  25777  distsava  25792  intvconlem1  25806  hdrmp  25809  cmppfd  25848  domcmpd  25849  codcmpd  25850  cmpasso  25876  cmpida  25877  cmpidb  25878  cmpassoh  25904  homgrf  25905  imonclem  25916  cmpmon  25918  iepiclem  25926  isepic  25927  idfisf  25944  issrc  25970  propsrc  25971  partarelt1  25999  inttarcar  26004  fnctartar  26010  fnctartar2  26011  prismorcset2  26021  cmpmor  26078  setiscat  26082  lemindclsbu  26098  indcls2  26099  clscnc  26113  pgapspf2  26156  gltpntl  26175  lineval5a  26191  lineval6a  26192  isconcl5a  26204  isconcl5ab  26205  isconcl6a  26206  isibg2aa  26215  isib2g1a1  26219  isibg1a2  26220  isibg2a  26221  isibg1a3a  26225  isibg1spa  26226  isibg1a5a  26227  bsstr  26231  nbssntr  26232  sgplpte21d  26239  segline  26244  pxysxy  26245  lppotoslem  26246  lppotos  26247  xsyysx  26248  nbssntrs  26250  pdiveql  26271  abhp  26276  elicc3  26331  nn0prpwlem  26341  nn0prpw  26342  fnessref  26396  neibastop2lem  26412  filnetlem4  26433  fzmul  26546  fdc  26558  seqpo  26560  incsequz  26561  isismty  26628  ismtybndlem  26633  heibor1lem  26636  ghomco  26676  zerdivemp1x  26689  pridlc  26799  ceqsex3OLD  26829  nelss  26854  incssnn0  26889  fphpd  27002  jm2.19lem3  27187  setindtr  27220  dfac21  27267  islssfg2  27272  mpaaeu  27458  psgnunilem4  27523  pm14.24  27735  stoweidlem26  27878  hirstL-ax3  27963  rexsb  28049  rexrsb  28050  2reu1  28067  afvres  28140  tz6.12-afv  28141  afvco2  28144  ndmaovdistr  28175  f1veqaeq  28188  mpt2xopoveqd  28203  elfznelfzo  28213  injresinjlem  28214  injresinj  28215  hashtpg  28217  hashgt12el  28218  hashgt12el2  28219  usgraeq12d  28245  usgraedgprv  28256  usgraedgrnv  28257  usgranloop  28258  usgra1v  28260  nbgraop  28274  nbusgra  28277  nbgranself2  28285  nb3graprlem1  28287  nbcusgra  28298  uvtxnbgra  28306  trlonprop  28341  pthdepisspth  28360  redwlk  28364  wlkdvspth  28366  cyclnspth  28376  cyclispthon  28378  fargshiftfo  28383  eupatrl  28385  usgrcyclnl1  28386  nvnencycllem  28389  3v3e3cycl1  28390  constr3trllem2  28397  4cycl4v4e  28412  4cycl4dv  28413  4cycl4dv4e  28414  frgra2v  28423  frgra3vlem1  28424  frgra3vlem2  28425  3vfriswmgralem  28428  3vfriswmgra  28429  3cyclfrgrarn1  28435  n4cyclfrgra  28440  ad5ant23  28531  ad5ant24  28532  ad5ant25  28533  ad5ant245  28534  ad5ant234  28535  ad5ant235  28536  sb5ALT  28587  truniALT  28604  onfrALTlem3  28608  ee223  28711  eel12131  28798  eel32131  28801  3imp231  28907  3orbi123VD  28942  sbc3orgVD  28943  exbirVD  28945  exbiriVD  28946  sbcim2gVD  28967  trsbcVD  28969  truniALTVD  28970  onfrALTlem3VD  28979  onfrALTlem2VD  28981  csbrngVD  28988  19.41rgVD  28994  a9e2eqVD  28999  a9e2ndeqVD  29001  2uasbanhVD  29003  sb5ALTVD  29005  vk15.4jVD  29006  ax12olem3aAUX7  29434  ax10lem4NEW7  29448  sb6rfNEW7  29564  sb56NEW7  29568  exsbNEW7  29571  ax11bNEW7  29594  ax12-3  29726  ax9lem2  29763  ax9lem5  29766  ax9lem15  29776  ax9vax9  29780  cdleme18d  31106  tendovalco  31576  cdlemn11pre  32022  dihord2pre  32037
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator