Theorem mpcom 32

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 27	. 2 |- ( ps -> ( ph -> ch ) )
4	1, 3	mpd 13	1 |- ( ps -> ch )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  syldan  266  ax16i  1738  ceqex  2671  peano2  4318  sotri  4720  relcoi1  4849  f1ocnv  5139  tz6.12c  5203  funbrfv  5212  fnbrfvb  5214  fvmptss2  5247  oprabid  5537  eloprabga  5591  unielxp  5800  f1o2ndf1  5849  tfrlem1  5923  freccl  5993  ecopovtrn  6203  ecopovtrng  6206  findcard2d  6348  findcard2sd  6349  ltexnqi  6507  prcdnql  6582  prcunqu  6583  prnmaxl  6586  prnminu  6587  ltprordil  6687  1idprl  6688  1idpru  6689  ltexprlemm  6698  ltexprlemopu  6701  ltexprlemru  6710  recexgt0sr  6858  mulgt0sr  6862  ltrenn  6931  nnindnn  6967  nnind  7930  nnmulcl  7935  nnnegz  8248  ublbneg  8548  ixxssxr  8769  ixxssixx  8771  iccshftri  8863  iccshftli  8865  iccdili  8867  icccntri  8869  1fv  8996  fzo1fzo0n0  9039  elfzonlteqm1  9066  ssfzo12  9080  flqeqceilz  9160  frec2uzltd  9189  frec2uzrdg  9195  iseqfveq2  9228  iseqshft2  9232  monoord  9235  iseqsplit  9238  iseqcaopr3  9240  iseqhomo  9248  cjre  9482  climeu  9817  climub  9864  bdfind  10071  bj-nn0sucALT  10103