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  1735  ceqex  2665  peano2  4261  sotri  4663  relcoi1  4792  f1ocnv  5082  tz6.12c  5146  funbrfv  5155  fnbrfvb  5157  fvmptss2  5190  oprabid  5480  eloprabga  5533  unielxp  5742  f1o2ndf1  5791  tfrlem1  5864  freccl  5932  ecopovtrn  6139  ecopovtrng  6142  ltexnqi  6392  prcdnql  6467  prcunqu  6468  prnmaxl  6471  prnminu  6472  ltprordil  6565  1idprl  6566  1idpru  6567  ltexprlemm  6574  ltexprlemopu  6577  ltexprlemru  6586  recexgt0sr  6701  mulgt0sr  6704  nnind  7711  nnmulcl  7716  nnnegz  8024  ublbneg  8324  ixxssxr  8539  ixxssixx  8541  iccshftri  8633  iccshftli  8635  iccdili  8637  icccntri  8639  1fv  8766  fzo1fzo0n0  8809  elfzonlteqm1  8836  ssfzo12  8850  frec2uzltd  8870  frec2uzrdg  8876  iseqfveq2  8905  cjre  9110  bdfind  9406  bj-nn0sucALT  9438