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

Theorem mpcom 32
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 27 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
41, 3mpd 14 1  |-  ( ps 
->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syldan  456  ax16i  1988  ceqex  2900  limomss  4663  elimasni  5042  sotri  5072  sotriOLD  5077  relcoi1  5203  unixpid  5209  f1ocnv  5487  tz6.12c  5549  funbrfv  5563  oprabid  5884  ndmovordi  6013  unielxp  6160  smogt  6386  oawordeulem  6554  omass  6580  ecopovtrn  6763  php  7047  unxpdom  7072  findcard3  7102  isfinite2  7117  cantnfval2  7372  cantnfle  7374  cantnfp1lem3  7384  cantnflem1  7393  cnfcom  7405  rankr1ai  7472  rankonidlem  7502  rankxplim2  7552  oncard  7595  ficardom  7596  cardne  7600  acnnum  7681  alephord2i  7706  cardaleph  7718  aceq3lem  7749  dfac5lem5  7756  dfac12lem3  7773  cdainf  7820  ackbij1lem16  7863  cfslb  7894  cfslb2n  7896  cfsmolem  7898  fin4i  7926  infpssr  7936  fin1a2lem6  8033  axdc3lem2  8079  axcclem  8085  ttukeylem6  8143  fodomb  8153  gchi  8248  fpwwe2lem5  8258  pwfseqlem4  8286  pwfseq  8288  inawina  8314  wunfi  8345  inar1  8399  ltexnq  8601  ltbtwnnq  8604  ltexprlem4  8665  ltexpri  8669  prlem936  8673  suplem1pr  8678  suplem2pr  8679  recexsrlem  8727  mulgt0sr  8729  map2psrpr  8734  supsr  8736  ledivp1i  9684  nnind  9766  nnmulcl  9771  nnnegz  10029  uzindOLD  10108  ublbneg  10304  xmulasslem  10607  ixxssixx  10672  iccshftri  10772  iccshftli  10774  iccdili  10776  icccntri  10778  seqp1  11063  seqcl2  11066  seqfveq2  11070  seqshft2  11074  monoord  11078  seqsplit  11081  seqcaopr3  11083  seqf1olem2a  11086  seqf1o  11089  seqid2  11094  seqhomo  11095  hashf1lem2  11396  seqcoll  11403  cjre  11626  climeu  12031  climub  12137  fsum2d  12236  fsumabs  12261  fsumrlim  12271  fsumo1  12272  fsumiun  12281  ruclem9  12518  sadcadd  12651  sadadd2  12653  saddisjlem  12657  smuval2  12675  smupval  12681  smueqlem  12683  smumullem  12685  exprmfct  12791  eulerthlem2  12852  pcmpt  12942  vdwlem10  13039  prmlem1a  13110  mreexexd  13552  letsr  14351  sylow1lem1  14911  efginvrel2  15038  efgsrel  15045  gsum2d  15225  dprdval  15240  ablfac1eulem  15309  pgpfac1  15317  pgpfac  15321  mplcoe1  16211  mplcoe3  16212  mplcoe2  16213  tg2  16705  neindisj2  16862  t1t0  17078  fiuncmp  17133  hmeof1o  17457  ist1-5lem  17513  t1r0  17514  alexsublem  17740  imasdsf1olem  17939  tgioo  18304  fsumcn  18376  voliunlem3  18911  itgfsum  19183  dvbsss  19254  dvmptfsum  19324  dvfsumlem2  19376  dvfsumlem4  19378  mpfaddcl  19428  mpfmulcl  19429  pf1addcl  19438  pf1mulcl  19439  plyco  19625  dgrcolem1  19656  dgrco  19658  dvntaylp  19752  taylthlem1  19754  jensen  20285  bposlem5  20529  lgsquad2lem2  20600  dchrisum0flb  20661  pntpbnd1  20737  pntlemf  20756  opidon2  20993  isexid2  20994  grpomndo  21015  elghomlem2  21031  rngoidmlem  21092  rngoueqz  21099  blocn2  21388  cvexchlem  22950  cdj3lem2b  23019  issgon  23486  subfacp1lem6  23718  cvmliftlem7  23824  cvmliftlem10  23827  eupath2  23906  relexp0  24027  relexpsucr  24028  relexpsucl  24030  relexprel  24033  relexpdm  24034  relexprn  24035  relexpadd  24037  relexpindlem  24038  relexpind  24039  rtrclreclem.trans  24045  rtrclreclem.min  24046  dfrtrcl2  24047  rtrclind  24048  pprodss4v  24426  funpartfv  24485  brbtwn  24529  brcgr  24530  segleantisym  24740  rankeq1o  24803  inpws1  25053  mapmapmap  25159  injsurinj  25160  prl  25178  prl2  25180  sege  25263  mxlmnl2  25281  defse3  25283  dfps2  25300  ablocomgrp  25353  grpodivfo  25385  grpodrcan  25386  grpodlcan  25387  rngodmeqrn  25430  mulinvsca  25491  glmrngo  25493  svs2  25498  truni2  25517  truni3  25518  intopcoaconlem3b  25549  intcont  25554  fil2ss  25568  prdnei  25584  limptlimpr2lem1  25585  islimrs4  25593  bwt2  25603  xrletr2  25629  lvsovso  25637  supnuf  25640  addcanrg  25678  negveud  25679  negveudr  25680  subctct  25865  tartarmap  25899  inttarcar  25912  carinttar  25913  fnctartar  25918  fnctartar2  25919  codcatfun  25945  grphidmor2  25964  cmp2morp  25969  cmp2morpcatt  25973  setiscat  25990  indcls2  26007  clscnc  26021  lineval5a  26099  lineval6a  26100  isconcl6a  26114  isconcl6ab  26115  isibg2aa  26123  isib2g1a1  26127  isibg2a  26129  isibg1a3a  26133  isibg1spa  26134  isibg1a5a  26135  bsstr  26139  nbssntr  26140  lppotoslem  26154  lppotos  26155  nbssntrs  26158  abhp  26184  mettrifi  26484  iscringd  26635  mzpadd  26827  mzpmul  26828  mzpcompact2  26841  dford3lem2  27131  aomclem6  27167  cnsrexpcl  27381  pmtrfrn  27411  ax10ext  27617  iotavalsb  27644  fmul01  27721  fmulcl  27722  fmuldfeqlem1  27723  fmuldfeq  27724  stoweidlem2  27762  stoweidlem3  27763  stoweidlem17  27777  stoweidlem21  27781  stoweidlem26  27786  stoweidlem31  27791  stoweidlem34  27794  stoweidlem48  27808  funressnfv  28002  afv0fv0  28023  afv0nbfvbi  28025  uslisumgra  28123  usisuslgra  28124  usgra0v  28128  usgra1v  28137  nbusgra  28154  iscusgra0  28165  cusgrauvtx  28179  3vfriswmgra  28194  bnj938  29042  bnj964  29048  bnj1052  29078  bnj1125  29095  cdlemk35s  31199  cdlemk39s  31201  cdlemk42  31203
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator