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  1904  ceqex  2930  sbcn1  3076  sbcim1  3077  sbcbi1  3078  sbcel21v  3093  ifnetruedc  3646  peano2  4687  sotri  5124  relcoi1  5260  f0rn0  5522  f1ocnv  5587  tz6.12c  5659  funbrfv  5672  fnbrfvb  5674  fvmptss2  5711  elfvmptrab1  5731  oprabid  6039  eloprabga  6097  elovmporab  6211  elovmporab1w  6212  relmptopab  6213  unielxp  6326  f1o2ndf1  6380  cnvoprab  6386  tfrlem1  6460  tfr1onlemaccex  6500  tfrcllemaccex  6513  ecopovtrn  6787  ecopovtrng  6790  findcard2d  7061  findcard2sd  7062  fidcenumlemr  7133  difinfsn  7278  nnnninfeq2  7307  ismkvnex  7333  cc3  7465  ltexnqi  7607  prcdnql  7682  prcunqu  7683  prnmaxl  7686  prnminu  7687  ltprordil  7787  1idprl  7788  1idpru  7789  ltexprlemm  7798  ltexprlemopu  7801  ltexprlemru  7810  recexgt0sr  7971  mulgt0sr  7976  ltrenn  8053  nnindnn  8091  nnind  9137  nnmulcl  9142  nnnegz  9460  supinfneg  9802  infsupneg  9803  ublbneg  9820  ixxssxr  10108  ixxssixx  10110  iccshftri  10203  iccshftli  10205  iccdili  10207  icccntri  10209  1fv  10347  fzo1fzo0n0  10395  elfzonlteqm1  10428  ssfzo12  10442  exbtwnzlemshrink  10480  flqeqceilz  10552  zmodidfzoimp  10588  modfzo0difsn  10629  frec2uzltd  10637  frec2uzrdg  10643  frecuzrdgg  10650  seq3clss  10705  seq3fveq2  10709  seqfveq2g  10711  seq3shft2  10715  seqshft2g  10716  monoord  10719  seq3split  10722  seqsplitg  10723  seq3caopr3  10725  seqcaopr3g  10726  seq3f1olemp  10749  seqf1oglem2a  10752  seqf1og  10755  seq3id2  10760  seq3homo  10761  seq3z  10762  seqhomog  10764  seqfeq4g  10765  ser3ge0  10770  exp3vallem  10774  modqexp  10900  fihashf1rn  11022  hashfzp1  11059  seq3coll  11077  swrdswrd  11252  pfxccatin12lem2a  11274  pfxccatin12  11280  swrdccat  11282  pfxccat3a  11285  swrdccatin1d  11290  swrdccatin2d  11291  cjre  11408  climeu  11822  climub  11870  fsum2d  11961  fsumabs  11991  fsumiun  12003  cvgratnnlemnexp  12050  cvgratnnlemmn  12051  prodfap0  12071  prodfrecap  12072  ntrivcvgap  12074  fprodabs  12142  fprod2d  12149  dvdsmod0  12319  p1modz1  12320  dvdsmodexp  12321  dvdsabseq  12373  mulsucdiv2z  12411  nno  12432  nn0o  12433  dfgcd2  12550  lcmgcdlem  12614  cncongr2  12641  exprmfct  12675  eulerthlemrprm  12766  eulerthlema  12767  dvdsprmpweqnn  12874  dvdsprmpweqle  12875  pcmpt  12881  ennnfoneleminc  12997  ennnfonelemkh  12998  ennnfonelemhf1o  12999  ennnfonelemhom  13001  nninfdclemlt  13037  setsn0fun  13084  insubm  13533  ghmghmrn  13815  srgpcomp  13968  ringrng  14014  gsumfzfsumlemm  14566  tg2  14749  hmeof1o  14998  tgioo  15243  dvmptfsum  15414  plycolemc  15447  perfectlem2  15689  gausslemma2dlem0i  15751  lgsquad2lem2  15776  2lgslem3  15795  2lgs  15798  2lgsoddprm  15807  umgrnloop  15931  usgredg2vlem2  16036  wlkv  16067  wlkl1loop  16099  wlk1walkdom  16100  uspgr2wlkeqi  16108  wlkres  16118  umgrclwwlkge2  16139  bdfind  16364  bj-nn0sucALT  16396  nninfsellemqall  16441