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

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

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syldan  282  ax16i  1911  ceqex  2953  sbcn1  3099  sbcim1  3100  sbcbi1  3101  sbcel21v  3116  ifnetruedc  3684  peano2  4742  sotri  5183  relcoi1  5319  f0rn0  5587  f1ocnv  5652  tz6.12c  5725  funbrfv  5739  fnbrfvb  5741  fvmptss2  5780  elfvmptrab1  5801  oprabid  6117  eloprabga  6175  elovmporab  6289  elovmporab1w  6290  relmptopab  6291  unielxp  6408  f1o2ndf1  6464  cnvoprab  6470  ressuppss  6494  tfrlem1  6579  tfr1onlemaccex  6619  tfrcllemaccex  6632  ecopovtrn  6906  ecopovtrng  6909  findcard2d  7195  findcard2sd  7196  fidcenumlemr  7272  fsuppimp  7292  difinfsn  7440  nnnninfeq2  7469  ismkvnex  7495  cc3  7634  ltexnqi  7776  prcdnql  7851  prcunqu  7852  prnmaxl  7855  prnminu  7856  ltprordil  7956  1idprl  7957  1idpru  7958  ltexprlemm  7967  ltexprlemopu  7970  ltexprlemru  7979  recexgt0sr  8140  mulgt0sr  8145  ltrenn  8222  nnindnn  8260  nnind  9320  nnmulcl  9325  nnnegz  9647  supinfneg  9995  infsupneg  9996  ublbneg  10013  ixxssxr  10302  ixxssixx  10304  iccshftri  10397  iccshftli  10399  iccdili  10401  icccntri  10403  1fv  10546  fzo1fzo0n0  10595  elfzonlteqm1  10628  ssfzo12  10642  exbtwnzlemshrink  10683  flqeqceilz  10755  zmodidfzoimp  10791  modfzo0difsn  10832  frec2uzltd  10840  frec2uzrdg  10846  frecuzrdgg  10853  seq3clss  10908  seq3fveq2  10912  seqfveq2g  10914  seq3shft2  10918  seqshft2g  10919  monoord  10922  seq3split  10925  seqsplitg  10926  seq3caopr3  10928  seqcaopr3g  10929  seq3f1olemp  10952  seqf1oglem2a  10955  seqf1og  10958  seq3id2  10963  seq3homo  10964  seq3z  10965  seqhomog  10967  seqfeq4g  10968  ser3ge0  10973  exp3vallem  10977  modqexp  11104  fihashf1rn  11227  hashfzp1  11265  seq3coll  11294  swrdswrd  11477  pfxccatin12lem2a  11499  pfxccatin12  11505  swrdccat  11507  pfxccat3a  11510  swrdccatin1d  11515  swrdccatin2d  11516  cjre  11647  climeu  12062  climub  12110  fsum2d  12202  fsumabs  12232  fsumiun  12244  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  prodfap0  12312  prodfrecap  12313  ntrivcvgap  12315  fprodabs  12383  fprod2d  12390  dvdsmod0  12560  p1modz1  12561  dvdsmodexp  12562  dvdsabseq  12614  mulsucdiv2z  12652  nno  12673  nn0o  12674  dfgcd2  12791  lcmgcdlem  12855  cncongr2  12882  exprmfct  12916  eulerthlemrprm  13007  eulerthlema  13008  dvdsprmpweqnn  13115  dvdsprmpweqle  13116  pcmpt  13122  ballotfilemfc0  13232  ennnfoneleminc  13302  ennnfonelemkh  13303  ennnfonelemhf1o  13304  ennnfonelemhom  13306  nninfdclemlt  13342  setsn0fun  13389  insubm  13792  ghmghmrn  14066  srgpcomp  14294  ringrng  14341  tg2  15161  hmeof1o  15410  tgioo  15655  dvmptfsum  15826  plycolemc  15859  perfectlem2  16114  gausslemma2dlem0i  16176  lgsquad2lem2  16201  2lgslem3  16220  2lgs  16223  2lgsoddprm  16232  umgrnloop  16357  usgredg2vlem2  16464  subgrprop  16500  wlkv  16567  wlkl1loop  16599  wlk1walkdom  16600  uspgr2wlkeqi  16608  wlkres  16620  umgrclwwlkge2  16643  clwwlknp  16658  clwwlkext2edg  16663  clwwlknun  16682  eupth2fi  16720  bdfind  16972  bj-nn0sucALT  17004  nninfsellemqall  17058