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  1907  ceqex  2947  sbcn1  3093  sbcim1  3094  sbcbi1  3095  sbcel21v  3110  ifnetruedc  3670  peano2  4722  sotri  5163  relcoi1  5299  f0rn0  5567  f1ocnv  5632  tz6.12c  5705  funbrfv  5718  fnbrfvb  5720  fvmptss2  5757  elfvmptrab1  5777  oprabid  6090  eloprabga  6148  elovmporab  6262  elovmporab1w  6263  relmptopab  6264  unielxp  6381  f1o2ndf1  6437  cnvoprab  6443  ressuppss  6467  tfrlem1  6552  tfr1onlemaccex  6592  tfrcllemaccex  6605  ecopovtrn  6879  ecopovtrng  6882  findcard2d  7161  findcard2sd  7162  fidcenumlemr  7238  fsuppimp  7258  difinfsn  7404  nnnninfeq2  7433  ismkvnex  7459  cc3  7598  ltexnqi  7740  prcdnql  7815  prcunqu  7816  prnmaxl  7819  prnminu  7820  ltprordil  7920  1idprl  7921  1idpru  7922  ltexprlemm  7931  ltexprlemopu  7934  ltexprlemru  7943  recexgt0sr  8104  mulgt0sr  8109  ltrenn  8186  nnindnn  8224  nnind  9270  nnmulcl  9275  nnnegz  9597  supinfneg  9945  infsupneg  9946  ublbneg  9963  ixxssxr  10252  ixxssixx  10254  iccshftri  10347  iccshftli  10349  iccdili  10351  icccntri  10353  1fv  10495  fzo1fzo0n0  10544  elfzonlteqm1  10577  ssfzo12  10591  exbtwnzlemshrink  10632  flqeqceilz  10704  zmodidfzoimp  10740  modfzo0difsn  10781  frec2uzltd  10789  frec2uzrdg  10795  frecuzrdgg  10802  seq3clss  10857  seq3fveq2  10861  seqfveq2g  10863  seq3shft2  10867  seqshft2g  10868  monoord  10871  seq3split  10874  seqsplitg  10875  seq3caopr3  10877  seqcaopr3g  10878  seq3f1olemp  10901  seqf1oglem2a  10904  seqf1og  10907  seq3id2  10912  seq3homo  10913  seq3z  10914  seqhomog  10916  seqfeq4g  10917  ser3ge0  10922  exp3vallem  10926  modqexp  11053  fihashf1rn  11176  hashfzp1  11214  seq3coll  11239  swrdswrd  11422  pfxccatin12lem2a  11444  pfxccatin12  11450  swrdccat  11452  pfxccat3a  11455  swrdccatin1d  11460  swrdccatin2d  11461  cjre  11592  climeu  12006  climub  12054  fsum2d  12146  fsumabs  12176  fsumiun  12188  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  prodfap0  12256  prodfrecap  12257  ntrivcvgap  12259  fprodabs  12327  fprod2d  12334  dvdsmod0  12504  p1modz1  12505  dvdsmodexp  12506  dvdsabseq  12558  mulsucdiv2z  12596  nno  12617  nn0o  12618  dfgcd2  12735  lcmgcdlem  12799  cncongr2  12826  exprmfct  12860  eulerthlemrprm  12951  eulerthlema  12952  dvdsprmpweqnn  13059  dvdsprmpweqle  13060  pcmpt  13066  ballotfilemfc0  13176  ennnfoneleminc  13246  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ennnfonelemhom  13250  nninfdclemlt  13286  setsn0fun  13333  insubm  13740  ghmghmrn  14016  srgpcomp  14233  ringrng  14279  gsumfzfsumlemm  14861  tg2  15051  hmeof1o  15300  tgioo  15545  dvmptfsum  15716  plycolemc  15749  perfectlem2  15994  gausslemma2dlem0i  16056  lgsquad2lem2  16081  2lgslem3  16100  2lgs  16103  2lgsoddprm  16112  umgrnloop  16237  usgredg2vlem2  16344  subgrprop  16380  wlkv  16447  wlkl1loop  16479  wlk1walkdom  16480  uspgr2wlkeqi  16488  wlkres  16500  umgrclwwlkge2  16523  clwwlknp  16538  clwwlkext2edg  16543  clwwlknun  16562  eupth2fi  16600  bdfind  16842  bj-nn0sucALT  16874  nninfsellemqall  16919