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  1881  ceqex  2900  sbcn1  3046  sbcim1  3047  sbcbi1  3048  sbcel21v  3063  ifnetruedc  3613  peano2  4643  sotri  5078  relcoi1  5214  f0rn0  5470  f1ocnv  5535  tz6.12c  5606  funbrfv  5617  fnbrfvb  5619  fvmptss2  5654  elfvmptrab1  5674  oprabid  5976  eloprabga  6032  elovmporab  6146  elovmporab1w  6147  unielxp  6260  f1o2ndf1  6314  cnvoprab  6320  tfrlem1  6394  tfr1onlemaccex  6434  tfrcllemaccex  6447  ecopovtrn  6719  ecopovtrng  6722  findcard2d  6988  findcard2sd  6989  fidcenumlemr  7057  difinfsn  7202  nnnninfeq2  7231  ismkvnex  7257  cc3  7380  ltexnqi  7522  prcdnql  7597  prcunqu  7598  prnmaxl  7601  prnminu  7602  ltprordil  7702  1idprl  7703  1idpru  7704  ltexprlemm  7713  ltexprlemopu  7716  ltexprlemru  7725  recexgt0sr  7886  mulgt0sr  7891  ltrenn  7968  nnindnn  8006  nnind  9052  nnmulcl  9057  nnnegz  9375  supinfneg  9716  infsupneg  9717  ublbneg  9734  ixxssxr  10022  ixxssixx  10024  iccshftri  10117  iccshftli  10119  iccdili  10121  icccntri  10123  1fv  10261  fzo1fzo0n0  10307  elfzonlteqm1  10339  ssfzo12  10353  exbtwnzlemshrink  10391  flqeqceilz  10463  zmodidfzoimp  10499  modfzo0difsn  10540  frec2uzltd  10548  frec2uzrdg  10554  frecuzrdgg  10561  seq3clss  10616  seq3fveq2  10620  seqfveq2g  10622  seq3shft2  10626  seqshft2g  10627  monoord  10630  seq3split  10633  seqsplitg  10634  seq3caopr3  10636  seqcaopr3g  10637  seq3f1olemp  10660  seqf1oglem2a  10663  seqf1og  10666  seq3id2  10671  seq3homo  10672  seq3z  10673  seqhomog  10675  seqfeq4g  10676  ser3ge0  10681  exp3vallem  10685  modqexp  10811  fihashf1rn  10933  hashfzp1  10969  seq3coll  10987  cjre  11193  climeu  11607  climub  11655  fsum2d  11746  fsumabs  11776  fsumiun  11788  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  prodfap0  11856  prodfrecap  11857  ntrivcvgap  11859  fprodabs  11927  fprod2d  11934  dvdsmod0  12104  p1modz1  12105  dvdsmodexp  12106  dvdsabseq  12158  mulsucdiv2z  12196  nno  12217  nn0o  12218  dfgcd2  12335  lcmgcdlem  12399  cncongr2  12426  exprmfct  12460  eulerthlemrprm  12551  eulerthlema  12552  dvdsprmpweqnn  12659  dvdsprmpweqle  12660  pcmpt  12666  ennnfoneleminc  12782  ennnfonelemkh  12783  ennnfonelemhf1o  12784  ennnfonelemhom  12786  nninfdclemlt  12822  setsn0fun  12869  insubm  13317  ghmghmrn  13599  srgpcomp  13752  ringrng  13798  gsumfzfsumlemm  14349  tg2  14532  hmeof1o  14781  tgioo  15026  dvmptfsum  15197  plycolemc  15230  perfectlem2  15472  gausslemma2dlem0i  15534  lgsquad2lem2  15559  2lgslem3  15578  2lgs  15581  2lgsoddprm  15590  bdfind  15882  bj-nn0sucALT  15914  nninfsellemqall  15952