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  1880  ceqex  2899  sbcn1  3045  sbcim1  3046  sbcbi1  3047  sbcel21v  3062  ifnetruedc  3612  peano2  4642  sotri  5077  relcoi1  5213  f0rn0  5469  f1ocnv  5534  tz6.12c  5605  funbrfv  5616  fnbrfvb  5618  fvmptss2  5653  elfvmptrab1  5673  oprabid  5975  eloprabga  6031  elovmporab  6145  elovmporab1w  6146  unielxp  6259  f1o2ndf1  6313  cnvoprab  6319  tfrlem1  6393  tfr1onlemaccex  6433  tfrcllemaccex  6446  ecopovtrn  6718  ecopovtrng  6721  findcard2d  6987  findcard2sd  6988  fidcenumlemr  7056  difinfsn  7201  nnnninfeq2  7230  ismkvnex  7256  cc3  7379  ltexnqi  7521  prcdnql  7596  prcunqu  7597  prnmaxl  7600  prnminu  7601  ltprordil  7701  1idprl  7702  1idpru  7703  ltexprlemm  7712  ltexprlemopu  7715  ltexprlemru  7724  recexgt0sr  7885  mulgt0sr  7890  ltrenn  7967  nnindnn  8005  nnind  9051  nnmulcl  9056  nnnegz  9374  supinfneg  9715  infsupneg  9716  ublbneg  9733  ixxssxr  10021  ixxssixx  10023  iccshftri  10116  iccshftli  10118  iccdili  10120  icccntri  10122  1fv  10260  fzo1fzo0n0  10305  elfzonlteqm1  10337  ssfzo12  10351  exbtwnzlemshrink  10389  flqeqceilz  10461  zmodidfzoimp  10497  modfzo0difsn  10538  frec2uzltd  10546  frec2uzrdg  10552  frecuzrdgg  10559  seq3clss  10614  seq3fveq2  10618  seqfveq2g  10620  seq3shft2  10624  seqshft2g  10625  monoord  10628  seq3split  10631  seqsplitg  10632  seq3caopr3  10634  seqcaopr3g  10635  seq3f1olemp  10658  seqf1oglem2a  10661  seqf1og  10664  seq3id2  10669  seq3homo  10670  seq3z  10671  seqhomog  10673  seqfeq4g  10674  ser3ge0  10679  exp3vallem  10683  modqexp  10809  fihashf1rn  10931  hashfzp1  10967  seq3coll  10985  cjre  11164  climeu  11578  climub  11626  fsum2d  11717  fsumabs  11747  fsumiun  11759  cvgratnnlemnexp  11806  cvgratnnlemmn  11807  prodfap0  11827  prodfrecap  11828  ntrivcvgap  11830  fprodabs  11898  fprod2d  11905  dvdsmod0  12075  p1modz1  12076  dvdsmodexp  12077  dvdsabseq  12129  mulsucdiv2z  12167  nno  12188  nn0o  12189  dfgcd2  12306  lcmgcdlem  12370  cncongr2  12397  exprmfct  12431  eulerthlemrprm  12522  eulerthlema  12523  dvdsprmpweqnn  12630  dvdsprmpweqle  12631  pcmpt  12637  ennnfoneleminc  12753  ennnfonelemkh  12754  ennnfonelemhf1o  12755  ennnfonelemhom  12757  nninfdclemlt  12793  setsn0fun  12840  insubm  13288  ghmghmrn  13570  srgpcomp  13723  ringrng  13769  gsumfzfsumlemm  14320  tg2  14503  hmeof1o  14752  tgioo  14997  dvmptfsum  15168  plycolemc  15201  perfectlem2  15443  gausslemma2dlem0i  15505  lgsquad2lem2  15530  2lgslem3  15549  2lgs  15552  2lgsoddprm  15561  bdfind  15844  bj-nn0sucALT  15876  nninfsellemqall  15914