MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpcom Structured version   Unicode version

Theorem mpcom 36
Description: Modus ponens inference with commutation of antecedents. (Contributed by NM, 17-Mar-1996.)
Hypotheses
Ref Expression
mpcom.1  |-  ( ps 
->  ph )
mpcom.2  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
mpcom  |-  ( ps 
->  ch )

Proof of Theorem mpcom
StepHypRef Expression
1 mpcom.1 . 2  |-  ( ps 
->  ph )
2 mpcom.2 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
32com12 31 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
41, 3mpd 15 1  |-  ( ps 
->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syldan  470  axc16i  2012  sbcn1  3229  sbcim1  3230  sbcbi1  3231  sbcel21v  3249  elimasni  5191  sotri  5220  sotriOLD  5225  relcoi1  5361  unixpid  5367  f1ocnv  5648  tz6.12c  5704  funbrfv  5725  f1dom3el3dif  5976  oprabid  6110  ndmovordi  6249  limomss  6476  unielxp  6607  f1o2ndf1  6675  smogt  6820  tfrlem1  6827  oawordeulem  6985  omass  7011  ecopovtrn  7195  php  7487  unxpdom  7512  findcard2d  7546  findcard3  7547  isfinite2  7562  fsuppimp  7618  fsuppunfi  7632  fsuppunbi  7633  fsuppres  7637  cantnfval2  7869  cantnfle  7871  cantnfp1lem3  7880  cantnflem1  7889  cantnfval2OLD  7899  cantnfleOLD  7901  cantnfp1lem3OLD  7906  cantnflem1OLD  7912  cnfcom  7925  cnfcomOLD  7933  rankr1ai  7997  rankonidlem  8027  rankxplim2  8079  oncard  8122  ficardom  8123  cardne  8127  acnnum  8214  alephord2i  8239  cardaleph  8251  aceq3lem  8282  dfac5lem5  8289  dfac12lem3  8306  cdainf  8353  ackbij1lem16  8396  cfslb  8427  cfslb2n  8429  cfsmolem  8431  fin4i  8459  infpssr  8469  fin1a2lem6  8566  axdc3lem2  8612  axcclem  8618  ttukeylem6  8675  fodomb  8685  gchi  8783  fpwwe2lem5  8793  pwfseqlem4  8821  pwfseq  8823  inawina  8849  wunfi  8880  inar1  8934  ltexnq  9136  ltbtwnnq  9139  ltexprlem4  9200  ltexpri  9204  prlem936  9208  suplem1pr  9213  suplem2pr  9214  recexsrlem  9262  mulgt0sr  9264  map2psrpr  9269  supsr  9271  eqlei  9476  eqlei2  9477  ledivp1i  10250  nnind  10332  nnmulcl  10337  nnnegz  10641  uzindOLD  10728  ublbneg  10931  xmulasslem  11240  ixxssixx  11306  iccshftri  11412  iccshftli  11414  iccdili  11416  icccntri  11418  1fv  11524  fzo1fzo0n0  11580  ssfzo12  11612  zmodidfzoimp  11730  seqp1  11813  seqcl2  11816  seqfveq2  11820  seqshft2  11824  monoord  11828  seqsplit  11831  seqcaopr3  11833  seqf1olem2a  11836  seqf1o  11839  seqid2  11844  seqhomo  11845  hashf1rn  12115  hashinfxadd  12140  hashle00  12150  hash2pr  12170  pr2pwpr  12175  hashf1lem2  12201  seqcoll  12208  brfi1uzind  12211  snopiswrd  12235  wrdlenfi  12250  swrdswrd  12346  swrdccatin12lem2a  12368  swrdccat  12376  swrdccatin1d  12382  swrdccatin2d  12383  swrdccatin12d  12384  repswccat  12415  cshwidxmod  12432  cjre  12620  climeu  13025  climub  13131  fsum2d  13230  fsumabs  13256  fsumrlim  13266  fsumo1  13267  fsumiun  13276  ruclem9  13512  sadcadd  13646  sadadd2  13648  saddisjlem  13652  smuval2  13670  smupval  13676  smueqlem  13678  smumullem  13680  exprmfct  13788  eulerthlem2  13849  pcmpt  13946  vdwlem10  14043  cshwsidrepsw  14112  cshwshashlem1  14114  prmlem1a  14126  mreexexd  14578  letsr  15389  pmtrfrn  15955  pmtr3ncom  15972  gsmtrcl  16013  sylow1lem1  16088  efginvrel2  16215  efgsrel  16222  cntzcmnss  16316  gsumzmhm  16420  gsumzoppg  16430  gsumunsnd  16442  gsum2dlem2  16452  gsum2dOLD  16454  dprdval  16475  dprdvalOLD  16477  ablfac1eulem  16563  pgpfac1  16571  pgpfac  16575  srgpcomp  16621  mplcoe1  17524  mplcoe3  17525  mplcoe3OLD  17526  mplcoe5lem  17527  mplcoe5  17528  mplcoe2OLD  17530  mpfaddcl  17600  mpfmulcl  17601  pf1addcl  17767  pf1mulcl  17768  evl1gsumd  17771  zrhpsgnelbas  18004  psgndiflemA  18011  mamufacex  18269  mavmulsolcl  18342  mdetunilem9  18406  cramerlem3  18475  tg2  18550  neindisj2  18707  neiptopnei  18716  t1t0  18932  fiuncmp  18987  bwthOLD  18994  hmeof1o  19317  ist1-5lem  19373  t1r0  19374  alexsublem  19596  imasdsf1olem  19928  tgioo  20353  fsumcn  20426  voliunlem3  21013  itgfsum  21284  dvbsss  21357  dvmptfsum  21427  dvfsumlem2  21479  dvfsumlem4  21481  plyco  21689  dgrcolem1  21720  dgrco  21722  dvntaylp  21816  taylthlem1  21818  jensen  22362  bposlem5  22607  lgsquad2lem2  22678  dchrisum0flb  22739  pntpbnd1  22815  pntlemf  22834  brbtwn  23113  brcgr  23114  uhgra0v  23212  umisuhgra  23229  uslisumgra  23253  usisuslgra  23254  usgra0v  23258  usgranloopv  23265  usgranloop  23266  usgra1v  23276  usgraidx2vlem2  23278  usgrafisindb0  23289  usgrafisindb1  23290  usgrafisinds  23294  usgrafisbase  23295  iscusgra0  23333  cusgrasize2inds  23353  cusgrafi  23358  2mwlk  23395  trliswlk  23406  2trllemE  23420  usgrnloop  23430  pthistrl  23439  spthispth  23440  pthdepisspth  23441  redwlk  23473  wlkdvspth  23475  crctistrl  23482  cyclispth  23483  cycliscrct  23484  cyclnspth  23485  cyclispthon  23487  fargshiftf  23490  fargshiftf1  23491  fargshiftfo  23492  usgrcyclnl1  23494  usgrcyclnl2  23495  nvnencycllem  23497  3v3e3cycl1  23498  constr3trllem5  23508  constr3trl  23513  constr3pth  23514  constr3cycl  23515  4cycl4v4e  23520  4cycl4dv4e  23522  cusconngra  23530  eupatrl  23557  eupath2  23569  opidon2  23779  isexid2  23780  grpomndo  23801  elghomlem2  23817  rngoidmlem  23878  rngoueqz  23885  blocn2  24176  cvexchlem  25740  cdj3lem2b  25809  cnvoprab  25991  nnindf  26057  issgon  26535  sitgclg  26697  sseqp1  26747  subfacp1lem6  27042  cvmliftlem7  27149  cvmliftlem10  27152  relexp0  27300  relexpsucr  27301  relexpsucl  27303  relexprel  27305  relexpdm  27306  relexprn  27307  relexpadd  27309  relexpindlem  27310  relexpind  27311  rtrclreclem.trans  27317  rtrclreclem.min  27318  dfrtrcl2  27319  rtrclind  27320  prodfn0  27378  prodfrec  27379  ntrivcvg  27381  fprodabs  27453  fprodefsum  27454  fprod2d  27461  pprodss4v  27884  segleantisym  28115  rankeq1o  28178  mblfinlem3  28401  mbfresfi  28409  mettrifi  28624  iscringd  28770  mzpadd  29045  mzpmul  29046  mzpcompact2  29060  dford3lem2  29347  aomclem6  29383  cnsrexpcl  29493  axc11next  29631  iotavalsb  29658  fmul01  29732  fmulcl  29733  fmuldfeqlem1  29734  fmuldfeq  29735  stoweidlem2  29768  stoweidlem3  29769  stoweidlem6  29772  stoweidlem8  29774  stoweidlem17  29783  stoweidlem19  29785  stoweidlem21  29787  stoweidlem26  29792  stoweidlem31  29797  stoweidlem43  29809  eu2ndop1stv  29997  funressnfv  30005  afv0fv0  30026  afv0nbfvbi  30028  f0rn0  30112  oprabv  30128  elovmpt2rab  30129  elovmpt2rab1  30130  elovmpt3rab1  30134  ssfz12  30168  fzoopth  30184  elfzonlteqm1  30196  hash3tr  30205  elovmptnn0wrd  30228  iswlkg  30256  2wlkeq  30259  wlkcpr  30261  edgwlk  30265  usgra2pthspth  30266  usgra2wlkspth  30269  spthdifv  30270  usgra2pth  30272  usgra2adedgspthlem2  30275  wwlknimp  30292  wwlkn0  30294  wlkiswwlk1  30295  wlkiswwlk2lem4  30299  wlkiswwlk2  30302  wlklniswwlkn2  30305  wwlkiswwlkn  30307  wwlknred  30326  wwlknext  30327  wwlknextbi  30328  wwlknredwwlkn0  30330  wwlkextwrd  30331  wwlkm1edg  30338  2spontn0vne  30377  usg2spthonot  30378  usg2spthonot0  30379  isclwlkg  30391  clwlkswlks  30394  clwwlkprop  30404  clwwlkgt0  30405  clwwlknimp  30410  clwlkisclwwlklem2a  30418  clwlkisclwwlklem1  30420  clwwlkext2edg  30435  clwwisshclww  30442  clwwnisshclwwn  30444  usghashecclwwlk  30480  wlkp1lenfislenp  30483  usgfidegfi  30498  usgravd00  30509  rgraprop  30516  rusgraprop  30517  rusgrargra  30518  cusgraisrusgra  30522  rusgrasn  30528  wwlkextproplem3  30533  rusgranumwlklem1  30538  3vfriswmgra  30568  3cyclfrgrarn1  30575  3cyclfrgrarn  30576  n4cyclfrgra  30581  frgranbnb  30583  frconngra  30584  vdfrgra0  30585  vdgfrgra0  30586  vdn0frgrav2  30587  vdgn0frgrav2  30588  usgn0fidegnn0  30593  frgrancvvdeqlem4  30597  frgrancvvdeqlem7  30600  frgrancvvdeqlemA  30601  frgrancvvdeqlemB  30602  frgrawopreglem2  30609  frgrawopreglem4  30611  frgrawopreglem5  30612  frgrawopreg  30613  frgraregorufr0  30616  frgraeu  30618  frg2wot1  30621  frg2woteqm  30623  frg2woteq  30624  frgregordn0  30634  numclwwlkun  30643  numclwwlk8  30679  frgrareggt1  30680  frgrareg  30681  frgraregord013  30682  frgraregord13  30683  frgraogt3nreg  30684  friendshipgt3  30685  friendship  30686  ztprmneprm  30709  psgnsn  30740  rng1ne0  30742  0rngnnzr  30747  lmod0rng  30748  scmsuppss  30754  coe1fzgsumd  30803  gsummoncoe1  30808  mat0dimcrng  30826  scmatsubcl  30844  scmatmulcl  30846  lcoel0  30893  ellcoellss  30900  lindslinindsimp2lem5  30927  ldepspr  30938  bnj938  31859  bnj964  31865  bnj1052  31895  bnj1125  31912  cdlemk35s  34474  cdlemk39s  34476  cdlemk42  34478
  Copyright terms: Public domain W3C validator