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  2021  sbcn1  3332  sbcim1  3333  sbcbi1  3334  sbcel21v  3352  elimasni  5294  sotri  5323  sotriOLD  5328  relcoi1  5464  unixpid  5470  f1ocnv  5751  tz6.12c  5808  funbrfv  5829  f1dom3el3dif  6080  oprabid  6214  ndmovordi  6354  limomss  6581  unielxp  6712  f1o2ndf1  6780  smogt  6928  tfrlem1  6935  oawordeulem  7093  omass  7119  ecopovtrn  7303  php  7595  unxpdom  7621  findcard2d  7655  findcard3  7656  isfinite2  7671  fsuppimp  7727  fsuppunfi  7741  fsuppunbi  7742  fsuppres  7746  cantnfval2  7978  cantnfle  7980  cantnfp1lem3  7989  cantnflem1  7998  cantnfval2OLD  8008  cantnfleOLD  8010  cantnfp1lem3OLD  8015  cantnflem1OLD  8021  cnfcom  8034  cnfcomOLD  8042  rankr1ai  8106  rankonidlem  8136  rankxplim2  8188  oncard  8231  ficardom  8232  cardne  8236  acnnum  8323  alephord2i  8348  cardaleph  8360  aceq3lem  8391  dfac5lem5  8398  dfac12lem3  8415  cdainf  8462  ackbij1lem16  8505  cfslb  8536  cfslb2n  8538  cfsmolem  8540  fin4i  8568  infpssr  8578  fin1a2lem6  8675  axdc3lem2  8721  axcclem  8727  ttukeylem6  8784  fodomb  8794  gchi  8892  fpwwe2lem5  8902  pwfseqlem4  8930  pwfseq  8932  inawina  8958  wunfi  8989  inar1  9043  ltexnq  9245  ltbtwnnq  9248  ltexprlem4  9309  ltexpri  9313  prlem936  9317  suplem1pr  9322  suplem2pr  9323  recexsrlem  9371  mulgt0sr  9373  map2psrpr  9378  supsr  9380  eqlei  9585  eqlei2  9586  ledivp1i  10359  nnind  10441  nnmulcl  10446  nnnegz  10750  uzindOLD  10837  ublbneg  11040  xmulasslem  11349  ixxssixx  11415  iccshftri  11521  iccshftli  11523  iccdili  11525  icccntri  11527  1fv  11633  fzo1fzo0n0  11689  ssfzo12  11721  zmodidfzoimp  11839  seqp1  11922  seqcl2  11925  seqfveq2  11929  seqshft2  11933  monoord  11937  seqsplit  11940  seqcaopr3  11942  seqf1olem2a  11945  seqf1o  11948  seqid2  11953  seqhomo  11954  hashf1rn  12224  hashinfxadd  12250  hashle00  12260  hash2pr  12280  pr2pwpr  12285  hashf1lem2  12311  seqcoll  12318  brfi1uzind  12321  snopiswrd  12345  wrdlenfi  12360  swrdswrd  12456  swrdccatin12lem2a  12478  swrdccat  12486  swrdccatin1d  12492  swrdccatin2d  12493  swrdccatin12d  12494  repswccat  12525  cshwidxmod  12542  cjre  12730  climeu  13135  climub  13241  fsum2d  13340  fsumabs  13366  fsumrlim  13376  fsumo1  13377  fsumiun  13386  ruclem9  13622  sadcadd  13756  sadadd2  13758  saddisjlem  13762  smuval2  13780  smupval  13786  smueqlem  13788  smumullem  13790  exprmfct  13898  eulerthlem2  13959  pcmpt  14056  vdwlem10  14153  cshwsidrepsw  14222  cshwshashlem1  14224  prmlem1a  14236  mreexexd  14688  letsr  15499  pmtrfrn  16066  pmtr3ncom  16083  gsmtrcl  16124  psgnsn  16128  sylow1lem1  16201  efginvrel2  16328  efgsrel  16335  cntzcmnss  16429  gsumzmhm  16535  gsumzoppg  16545  gsumunsnd  16557  gsum2dlem2  16567  gsum2dOLD  16569  dprdval  16590  dprdvalOLD  16592  ablfac1eulem  16678  pgpfac1  16686  pgpfac  16690  srgpcomp  16736  rimf1o  16929  rimrhm  16930  mplcoe1  17651  mplcoe3  17652  mplcoe3OLD  17653  mplcoe5lem  17654  mplcoe5  17655  mplcoe2OLD  17657  mpfaddcl  17727  mpfmulcl  17728  pf1addcl  17896  pf1mulcl  17897  evl1gsumd  17900  zrhpsgnelbas  18133  psgndiflemA  18140  mamufacex  18398  mavmulsolcl  18473  mdetunilem9  18542  cramerlem3  18611  tg2  18686  neindisj2  18843  neiptopnei  18852  t1t0  19068  fiuncmp  19123  bwthOLD  19130  hmeof1o  19453  ist1-5lem  19509  t1r0  19510  alexsublem  19732  imasdsf1olem  20064  tgioo  20489  fsumcn  20562  voliunlem3  21149  itgfsum  21420  dvbsss  21493  dvmptfsum  21563  dvfsumlem2  21615  dvfsumlem4  21617  plyco  21825  dgrcolem1  21856  dgrco  21858  dvntaylp  21952  taylthlem1  21954  jensen  22498  bposlem5  22743  lgsquad2lem2  22814  dchrisum0flb  22875  pntpbnd1  22951  pntlemf  22970  brbtwn  23280  brcgr  23281  uhgra0v  23379  umisuhgra  23396  uslisumgra  23420  usisuslgra  23421  usgra0v  23425  usgranloopv  23432  usgranloop  23433  usgra1v  23443  usgraidx2vlem2  23445  usgrafisindb0  23456  usgrafisindb1  23457  usgrafisinds  23461  usgrafisbase  23462  iscusgra0  23500  cusgrasize2inds  23520  cusgrafi  23525  2mwlk  23562  trliswlk  23573  2trllemE  23587  usgrnloop  23597  pthistrl  23606  spthispth  23607  pthdepisspth  23608  redwlk  23640  wlkdvspth  23642  crctistrl  23649  cyclispth  23650  cycliscrct  23651  cyclnspth  23652  cyclispthon  23654  fargshiftf  23657  fargshiftf1  23658  fargshiftfo  23659  usgrcyclnl1  23661  usgrcyclnl2  23662  nvnencycllem  23664  3v3e3cycl1  23665  constr3trllem5  23675  constr3trl  23680  constr3pth  23681  constr3cycl  23682  4cycl4v4e  23687  4cycl4dv4e  23689  cusconngra  23697  eupatrl  23724  eupath2  23736  opidon2  23946  isexid2  23947  grpomndo  23968  elghomlem2  23984  rngoidmlem  24045  rngoueqz  24052  blocn2  24343  cvexchlem  25907  cdj3lem2b  25976  cnvoprab  26157  nnindf  26223  issgon  26700  sitgclg  26862  sseqp1  26912  subfacp1lem6  27207  cvmliftlem7  27314  cvmliftlem10  27317  relexp0  27465  relexpsucr  27466  relexpsucl  27468  relexprel  27470  relexpdm  27471  relexprn  27472  relexpadd  27474  relexpindlem  27475  relexpind  27476  rtrclreclem.trans  27482  rtrclreclem.min  27483  dfrtrcl2  27484  rtrclind  27485  prodfn0  27543  prodfrec  27544  ntrivcvg  27546  fprodabs  27618  fprodefsum  27619  fprod2d  27626  pprodss4v  28049  segleantisym  28280  rankeq1o  28343  mblfinlem3  28568  mbfresfi  28576  mettrifi  28791  iscringd  28937  mzpadd  29212  mzpmul  29213  mzpcompact2  29227  dford3lem2  29514  aomclem6  29550  cnsrexpcl  29660  axc11next  29798  iotavalsb  29825  fmul01  29899  fmulcl  29900  fmuldfeqlem1  29901  fmuldfeq  29902  stoweidlem2  29935  stoweidlem3  29936  stoweidlem6  29939  stoweidlem8  29941  stoweidlem17  29950  stoweidlem19  29952  stoweidlem21  29954  stoweidlem26  29959  stoweidlem31  29964  stoweidlem43  29976  eu2ndop1stv  30164  funressnfv  30172  afv0fv0  30193  afv0nbfvbi  30195  f0rn0  30279  oprabv  30295  elovmpt2rab  30296  elovmpt2rab1  30297  elovmpt3rab1  30301  ssfz12  30335  fzoopth  30351  elfzonlteqm1  30363  hash3tr  30372  elovmptnn0wrd  30395  iswlkg  30423  2wlkeq  30426  wlkcpr  30428  edgwlk  30432  usgra2pthspth  30433  usgra2wlkspth  30436  spthdifv  30437  usgra2pth  30439  usgra2adedgspthlem2  30442  wwlknimp  30459  wwlkn0  30461  wlkiswwlk1  30462  wlkiswwlk2lem4  30466  wlkiswwlk2  30469  wlklniswwlkn2  30472  wwlkiswwlkn  30474  wwlknred  30493  wwlknext  30494  wwlknextbi  30495  wwlknredwwlkn0  30497  wwlkextwrd  30498  wwlkm1edg  30505  2spontn0vne  30544  usg2spthonot  30545  usg2spthonot0  30546  isclwlkg  30558  clwlkswlks  30561  clwwlkprop  30571  clwwlkgt0  30572  clwwlknimp  30577  clwlkisclwwlklem2a  30585  clwlkisclwwlklem1  30587  clwwlkext2edg  30602  clwwisshclww  30609  clwwnisshclwwn  30611  usghashecclwwlk  30647  wlkp1lenfislenp  30650  usgfidegfi  30665  usgravd00  30676  rgraprop  30683  rusgraprop  30684  rusgrargra  30685  cusgraisrusgra  30689  rusgrasn  30695  wwlkextproplem3  30700  rusgranumwlklem1  30705  3vfriswmgra  30735  3cyclfrgrarn1  30742  3cyclfrgrarn  30743  n4cyclfrgra  30748  frgranbnb  30750  frconngra  30751  vdfrgra0  30752  vdgfrgra0  30753  vdn0frgrav2  30754  vdgn0frgrav2  30755  usgn0fidegnn0  30760  frgrancvvdeqlem4  30764  frgrancvvdeqlem7  30767  frgrancvvdeqlemA  30768  frgrancvvdeqlemB  30769  frgrawopreglem2  30776  frgrawopreglem4  30778  frgrawopreglem5  30779  frgrawopreg  30780  frgraregorufr0  30783  frgraeu  30785  frg2wot1  30788  frg2woteqm  30790  frg2woteq  30791  frgregordn0  30801  numclwwlkun  30810  numclwwlk8  30846  frgrareggt1  30847  frgrareg  30848  frgraregord013  30849  frgraregord13  30850  frgraogt3nreg  30851  friendshipgt3  30852  friendship  30853  ztprmneprm  30877  rng1ne0  30911  0rngnnzr  30916  lmod0rng  30917  scmsuppss  30923  mptnn0fsuppr  30941  telescfzgsum  30951  coe1ae0  30974  coe1fzgsumd  30980  gsummoncoe1  30985  ply1mulgsumlem1  30986  ply1mulgsumlem2  30987  mat0dimcrng  31020  scmatsubcl  31038  scmatmulcl  31040  lcoel0  31069  ellcoellss  31076  lindslinindsimp2lem5  31103  ldepspr  31114  pmatcollpw4fi1  31244  pmattomply1fo  31268  chmaidscmat  31302  fvmptnn04if  31303  chfacfscmul0  31312  chfacfpmmul0  31316  cpmadugsumlemF  31330  bnj938  32230  bnj964  32236  bnj1052  32266  bnj1125  32283  cdlemk35s  34887  cdlemk39s  34889  cdlemk42  34891
  Copyright terms: Public domain W3C validator