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 )

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  282  ax16i  1906  ceqex  2933  sbcn1  3079  sbcim1  3080  sbcbi1  3081  sbcel21v  3096  ifnetruedc  3649  peano2  4693  sotri  5132  relcoi1  5268  f0rn0  5531  f1ocnv  5596  tz6.12c  5669  funbrfv  5682  fnbrfvb  5684  fvmptss2  5721  elfvmptrab1  5741  oprabid  6049  eloprabga  6107  elovmporab  6221  elovmporab1w  6222  relmptopab  6223  unielxp  6336  f1o2ndf1  6392  cnvoprab  6398  tfrlem1  6473  tfr1onlemaccex  6513  tfrcllemaccex  6526  ecopovtrn  6800  ecopovtrng  6803  findcard2d  7079  findcard2sd  7080  fidcenumlemr  7153  difinfsn  7298  nnnninfeq2  7327  ismkvnex  7353  cc3  7486  ltexnqi  7628  prcdnql  7703  prcunqu  7704  prnmaxl  7707  prnminu  7708  ltprordil  7808  1idprl  7809  1idpru  7810  ltexprlemm  7819  ltexprlemopu  7822  ltexprlemru  7831  recexgt0sr  7992  mulgt0sr  7997  ltrenn  8074  nnindnn  8112  nnind  9158  nnmulcl  9163  nnnegz  9481  supinfneg  9828  infsupneg  9829  ublbneg  9846  ixxssxr  10134  ixxssixx  10136  iccshftri  10229  iccshftli  10231  iccdili  10233  icccntri  10235  1fv  10373  fzo1fzo0n0  10421  elfzonlteqm1  10454  ssfzo12  10468  exbtwnzlemshrink  10507  flqeqceilz  10579  zmodidfzoimp  10615  modfzo0difsn  10656  frec2uzltd  10664  frec2uzrdg  10670  frecuzrdgg  10677  seq3clss  10732  seq3fveq2  10736  seqfveq2g  10738  seq3shft2  10742  seqshft2g  10743  monoord  10746  seq3split  10749  seqsplitg  10750  seq3caopr3  10752  seqcaopr3g  10753  seq3f1olemp  10776  seqf1oglem2a  10779  seqf1og  10782  seq3id2  10787  seq3homo  10788  seq3z  10789  seqhomog  10791  seqfeq4g  10792  ser3ge0  10797  exp3vallem  10801  modqexp  10927  fihashf1rn  11049  hashfzp1  11087  seq3coll  11105  swrdswrd  11285  pfxccatin12lem2a  11307  pfxccatin12  11313  swrdccat  11315  pfxccat3a  11318  swrdccatin1d  11323  swrdccatin2d  11324  cjre  11442  climeu  11856  climub  11904  fsum2d  11995  fsumabs  12025  fsumiun  12037  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  prodfap0  12105  prodfrecap  12106  ntrivcvgap  12108  fprodabs  12176  fprod2d  12183  dvdsmod0  12353  p1modz1  12354  dvdsmodexp  12355  dvdsabseq  12407  mulsucdiv2z  12445  nno  12466  nn0o  12467  dfgcd2  12584  lcmgcdlem  12648  cncongr2  12675  exprmfct  12709  eulerthlemrprm  12800  eulerthlema  12801  dvdsprmpweqnn  12908  dvdsprmpweqle  12909  pcmpt  12915  ennnfoneleminc  13031  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ennnfonelemhom  13035  nninfdclemlt  13071  setsn0fun  13118  insubm  13567  ghmghmrn  13849  srgpcomp  14002  ringrng  14048  gsumfzfsumlemm  14600  tg2  14783  hmeof1o  15032  tgioo  15277  dvmptfsum  15448  plycolemc  15481  perfectlem2  15723  gausslemma2dlem0i  15785  lgsquad2lem2  15810  2lgslem3  15829  2lgs  15832  2lgsoddprm  15841  umgrnloop  15966  usgredg2vlem2  16073  subgrprop  16109  wlkv  16176  wlkl1loop  16208  wlk1walkdom  16209  uspgr2wlkeqi  16217  wlkres  16229  umgrclwwlkge2  16252  clwwlknp  16267  clwwlkext2edg  16272  clwwlknun  16291  bdfind  16541  bj-nn0sucALT  16573  nninfsellemqall  16617