Theorem mpcom 38

Description: Modus ponens inference with commutation of antecedents. Commuted form of mpd 15. (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

Step	Hyp	Ref	Expression
1		mpcom.1	. 2 |- ( ps -> ph )
2		mpcom.2	. . 3 |- ( ph -> ( ps -> ch ) )
3	2	com12 32	. 2 |- ( ps -> ( ph -> ch ) )
4	1, 3	mpd 15	1 |- ( ps -> ch )

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  487  axc16i  2322  sbcn1  3481  sbcim1  3482  sbcbi1  3483  sbcel21v  3497  elimasni  5492  sotri  5523  unixpid  5670  f0rn0  6090  f1ocnv  6149  tz6.12c  6213  funbrfv  6234  funopsn  6413  f1dom3el3dif  6526  oprabid  6677  oprabv  6703  ndmovordi  6825  elovmpt2rab  6880  elovmpt2rab1  6881  elovmpt3rab1  6893  limomss  7070  unielxp  7204  bropfvvvvlem  7256  f1o2ndf1  7285  smogt  7464  tfrlem1  7472  oawordeulem  7634  omass  7660  ecopovtrn  7850  php  8144  unxpdom  8167  findcard2d  8202  findcard3  8203  isfinite2  8218  fsuppimp  8281  fsuppunfi  8295  fsuppunbi  8296  fsuppres  8300  cantnfval2  8566  cantnfle  8568  cantnfp1lem3  8577  cantnflem1  8586  cnfcom  8597  rankr1ai  8661  rankonidlem  8691  rankxplim2  8743  oncard  8786  ficardom  8787  cardne  8791  acnnum  8875  alephord2i  8900  cardaleph  8912  aceq3lem  8943  dfac5lem5  8950  dfac12lem3  8967  cdainf  9014  ackbij1lem16  9057  cfslb  9088  cfslb2n  9090  cfsmolem  9092  fin4i  9120  infpssr  9130  fin1a2lem6  9227  axdc3lem2  9273  axcclem  9279  ttukeylem6  9336  fodomb  9348  gchi  9446  fpwwe2lem5  9456  pwfseqlem4  9484  pwfseq  9486  inawina  9512  wunfi  9543  inar1  9597  ltexnq  9797  ltbtwnnq  9800  ltexprlem4  9861  ltexpri  9865  prlem936  9869  suplem1pr  9874  suplem2pr  9875  recexsrlem  9924  mulgt0sr  9926  map2psrpr  9931  supsr  9933  eqlei  10147  eqlei2  10148  ledivp1i  10949  nnind  11038  nnmulcl  11043  nn0ge2m1nn  11360  nnnegz  11380  ublbneg  11773  xmulasslem  12115  ixxssixx  12189  iccshftri  12307  iccshftli  12309  iccdili  12311  icccntri  12313  elfz1b  12409  fzo1fzo0n0  12518  elfzonlteqm1  12543  elfzo0l  12558  ssfzo12  12561  elfzo1elm1fzo0  12569  elfzr  12581  elfzlmr  12582  zmodidfzoimp  12700  mptnn0fsuppr  12799  seqp1  12816  seqcl2  12819  seqfveq2  12823  seqshft2  12827  monoord  12831  seqsplit  12834  seqcaopr3  12836  seqf1olem2a  12839  seqf1o  12842  seqid2  12847  seqhomo  12848  hashf1rn  13142  hashf1rnOLD  13143  hashinfxadd  13174  hashf1lem2  13240  seqcoll  13248  hash2pr  13251  pr2pwpr  13261  hashge2el2difr  13263  hash3tr  13272  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  elovmptnn0wrd  13348  swrdswrd  13460  swrdccatin12lem2a  13485  swrdccat  13493  swrdccatin1d  13499  swrdccatin2d  13500  swrdccatin12d  13501  repswccat  13532  cshwidxmod  13549  relexpsucnnr  13765  rtrclreclem3  13800  rtrclreclem4  13801  dfrtrcl2  13802  relexpindlem  13803  relexpind  13804  rtrclind  13805  cjre  13879  climeu  14286  climub  14392  fsum2d  14502  fsumabs  14533  fsumrlim  14543  fsumo1  14544  fsumiun  14553  prodfn0  14626  prodfrec  14627  ntrivcvg  14629  fprodabs  14704  fprod2d  14711  fprodefsum  14825  ruclem9  14967  dvdsabseq  15035  mod2eq1n2dvds  15071  mulsucdiv2z  15077  nno  15098  nn0o  15099  sadcadd  15180  sadadd2  15182  saddisjlem  15186  smuval2  15204  smupval  15210  smueqlem  15212  smumullem  15214  dfgcd2  15263  lcmgcdlem  15319  lcmftp  15349  exprmfct  15416  eulerthlem2  15487  dvdsprmpweqnn  15589  dvdsprmpweqle  15590  pcmpt  15596  vdwlem10  15694  cshwsidrepsw  15800  cshwshashlem1  15802  prmlem1a  15813  setsn0fun  15895  ressval3d  15937  mreexexd  16308  mreexexdOLD  16309  letsr  17227  ghmghmrn  17679  pmtrfrn  17878  pmtr3ncom  17895  gsmtrcl  17936  psgnsn  17940  sylow1lem1  18013  efginvrel2  18140  efgsrel  18147  cntzcmnss  18246  gsumzoppg  18344  gsum2dlem2  18370  telgsumfzs  18386  dprdval  18402  ablfac1eulem  18471  pgpfac1  18479  pgpfac  18483  srgpcomp  18532  ring1ne0  18591  rimf1o  18734  rimrhm  18735  brric2  18745  0ringnnzr  19269  mplcoe1  19465  mplcoe3  19466  mplcoe5lem  19467  mplcoe5  19468  mpfaddcl  19534  mpfmulcl  19535  coe1ae0  19586  coe1fzgsumd  19672  gsummoncoe1  19674  pf1addcl  19717  pf1mulcl  19718  evl1gsumd  19721  zrhpsgnelbas  19940  psgndiflemA  19947  mamufacex  20195  mat0dimcrng  20276  mavmulsolcl  20357  mdetunilem9  20426  cramerlem3  20495  pmatcollpw3fi1  20593  pm2mpfo  20619  chmaidscmat  20653  chfacfscmul0  20663  chfacfpmmul0  20667  cpmadugsumlemF  20681  tg2  20769  neindisj2  20927  neiptopnei  20936  t1t0  21152  fiuncmp  21207  hmeof1o  21567  ist1-5lem  21623  t1r0  21624  alexsublem  21848  imasdsf1olem  22178  tgioo  22599  fsumcn  22673  voliunlem3  23320  itgfsum  23593  dvbsss  23666  dvmptfsum  23738  dvfsumlem2  23790  dvfsumlem4  23792  plyco  23997  dgrcolem1  24029  dgrco  24031  dvntaylp  24125  taylthlem1  24127  jensen  24715  bposlem5  25013  lgsqrmodndvds  25078  gausslemma2dlem0i  25089  gausslemma2dlem4  25094  lgsquad2lem2  25110  2lgslem3  25129  2lgs  25132  2lgsoddprm  25141  dchrisum0flb  25199  pntpbnd1  25275  pntlemf  25294  brbtwn  25779  brcgr  25780  umgrnloopv  26001  umgrnloop  26003  usgrnloopvALT  26093  usgrnloopALT  26095  usgredg2vlem2  26118  subgrprop  26165  uvtxaisvtx  26289  vtxnbuvtx  26291  uvtxanbgrvtx  26293  cusgrsize2inds  26349  rgrprop  26456  rusgrprop  26458  wlkprop  26507  wlkvtxeledg  26519  wlkeq  26529  wlkl1loop  26534  wlk1walk  26535  uspgr2wlkeqi  26544  wlkreslem  26566  wlkres  26567  redwlk  26569  lfgrwlknloop  26586  2pthnloop  26627  usgr2trlncl  26656  usgr2pth  26660  clwlkcompim  26676  uspgrn2crct  26700  crctcshwlkn0  26713  wwlknp  26734  wwlkswwlksn  26750  wlkiswwlks2lem4  26758  wlkiswwlks2  26761  wlklnwwlkln2lem  26768  wwlksnext  26788  wwlksnextbi  26789  wwlksnredwwlkn0  26791  wwlksnextwrd  26792  clwwlknp  26887  clwwlkclwwlkn  26891  clwlkclwwlklem2a  26899  clwlkclwwlklem2  26901  clwwlksext2edg  26923  clwwisshclwws  26928  clwwnisshclwwsn  26930  umgrhashecclwwlk  26955  clwwlksnun  26974  1pthond  27004  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  eupth2  27099  3vfriswmgr  27142  3cyclfrgrrn1  27149  n4cyclfrgr  27155  frgrnbnb  27157  frgrncvvdeqlem3  27165  frgrncvvdeqlem6  27168  frgrncvvdeqlem7  27169  frgrncvvdeqlem8  27170  frgrwopreglem4a  27174  frgrwopreg  27187  frgrregorufr0  27188  frgr2wwlkeqm  27195  numclwwlk8  27250  frgrreggt1  27251  frgrregord013  27253  frgrregord13  27254  frgrogt3nreg  27255  friendshipgt3  27256  friendship  27257  blocn2  27663  cvexchlem  29227  cdj3lem2b  29296  cnvoprab  29498  nnindf  29565  issgon  30186  sitgclg  30404  sseqp1  30457  bnj938  31007  bnj964  31013  bnj1052  31043  bnj1125  31060  subfacp1lem6  31167  cvmliftlem7  31273  cvmliftlem10  31276  mclsrcl  31458  pprodss4v  31991  segleantisym  32222  rankeq1o  32278  bj-restv  33048  iooelexlt  33210  relowlssretop  33211  rdgeqoa  33218  matunitlindflem1  33405  poimirlem22  33431  poimirlem25  33434  poimirlem28  33437  poimirlem31  33440  mblfinlem3  33448  mbfresfi  33456  mettrifi  33553  opidon2OLD  33653  isexid2  33654  grpomndo  33674  elghomlem2OLD  33685  rngoidmlem  33735  rngoueqz  33739  iscringd  33797  cdlemk35s  36225  cdlemk39s  36227  cdlemk42  36229  mzpadd  37301  mzpmul  37302  mzpcompact2  37315  dford3lem2  37594  aomclem6  37629  cnsrexpcl  37735  relexpss1d  37997  iunrelexpmin1  38000  iunrelexpmin2  38004  nzin  38517  axc11next  38607  iotavalsb  38634  ssdec  39265  fperiodmullem  39517  fmul01  39812  fmulcl  39813  fmuldfeqlem1  39814  fmuldfeq  39815  fprodcnlem  39831  iblspltprt  40189  itgspltprt  40195  stoweidlem2  40219  stoweidlem3  40220  stoweidlem6  40223  stoweidlem8  40225  stoweidlem17  40234  stoweidlem19  40236  stoweidlem21  40238  stoweidlem26  40243  stoweidlem31  40248  stoweidlem43  40260  fourierdlem42  40366  eu2ndop1stv  41202  funressnfv  41208  afv0fv0  41229  afv0nbfvbi  41231  nelbrim  41292  ssfz12  41324  fzoopth  41337  smonoord  41341  iccpartiltu  41358  iccpartigtl  41359  iccelpart  41369  icceuelpart  41372  fargshiftf  41376  fargshiftf1  41377  fargshiftfo  41378  lighneallem4  41527  mogoldbblem  41629  sbgoldbwt  41665  bgoldbtbndlem2  41694  bgoldbtbndlem4  41696  tgoldbach  41705  tgoldbachOLD  41712  upwlkwlk  41720  sprel  41734  sprsymrelf1lem  41741  sprsymrelfolem2  41743  clcllaw  41827  intop  41839  clintop  41844  assintop  41845  assintopcllaw  41848  lmod0rng  41868  ringrng  41879  rngimf1o  41905  rngimrnghm  41906  ztprmneprm  42125  scmsuppss  42153  ply1mulgsumlem1  42174  ply1mulgsumlem2  42175  lcoel0  42217  ellcoellss  42224  lindslinindsimp2lem5  42251  ldepspr  42262  flnn0div2ge  42327  nnolog2flm1  42384  blengt1fldiv2p1  42387  dignn0flhalf  42412