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  2944  sbcn1  3090  sbcim1  3091  sbcbi1  3092  sbcel21v  3107  ifnetruedc  3666  peano2  4717  sotri  5158  relcoi1  5294  f0rn0  5562  f1ocnv  5627  tz6.12c  5700  funbrfv  5713  fnbrfvb  5715  fvmptss2  5752  elfvmptrab1  5772  oprabid  6082  eloprabga  6140  elovmporab  6254  elovmporab1w  6255  relmptopab  6256  unielxp  6368  f1o2ndf1  6424  cnvoprab  6430  ressuppss  6454  tfrlem1  6539  tfr1onlemaccex  6579  tfrcllemaccex  6592  ecopovtrn  6866  ecopovtrng  6869  findcard2d  7148  findcard2sd  7149  fidcenumlemr  7225  fsuppimp  7245  difinfsn  7391  nnnninfeq2  7420  ismkvnex  7446  cc3  7582  ltexnqi  7724  prcdnql  7799  prcunqu  7800  prnmaxl  7803  prnminu  7804  ltprordil  7904  1idprl  7905  1idpru  7906  ltexprlemm  7915  ltexprlemopu  7918  ltexprlemru  7927  recexgt0sr  8088  mulgt0sr  8093  ltrenn  8170  nnindnn  8208  nnind  9253  nnmulcl  9258  nnnegz  9580  supinfneg  9927  infsupneg  9928  ublbneg  9945  ixxssxr  10233  ixxssixx  10235  iccshftri  10328  iccshftli  10330  iccdili  10332  icccntri  10334  1fv  10473  fzo1fzo0n0  10522  elfzonlteqm1  10555  ssfzo12  10569  exbtwnzlemshrink  10608  flqeqceilz  10680  zmodidfzoimp  10716  modfzo0difsn  10757  frec2uzltd  10765  frec2uzrdg  10771  frecuzrdgg  10778  seq3clss  10833  seq3fveq2  10837  seqfveq2g  10839  seq3shft2  10843  seqshft2g  10844  monoord  10847  seq3split  10850  seqsplitg  10851  seq3caopr3  10853  seqcaopr3g  10854  seq3f1olemp  10877  seqf1oglem2a  10880  seqf1og  10883  seq3id2  10888  seq3homo  10889  seq3z  10890  seqhomog  10892  seqfeq4g  10893  ser3ge0  10898  exp3vallem  10902  modqexp  11028  fihashf1rn  11151  hashfzp1  11189  seq3coll  11214  swrdswrd  11397  pfxccatin12lem2a  11419  pfxccatin12  11425  swrdccat  11427  pfxccat3a  11430  swrdccatin1d  11435  swrdccatin2d  11436  cjre  11567  climeu  11981  climub  12029  fsum2d  12121  fsumabs  12151  fsumiun  12163  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  prodfap0  12231  prodfrecap  12232  ntrivcvgap  12234  fprodabs  12302  fprod2d  12309  dvdsmod0  12479  p1modz1  12480  dvdsmodexp  12481  dvdsabseq  12533  mulsucdiv2z  12571  nno  12592  nn0o  12593  dfgcd2  12710  lcmgcdlem  12774  cncongr2  12801  exprmfct  12835  eulerthlemrprm  12926  eulerthlema  12927  dvdsprmpweqnn  13034  dvdsprmpweqle  13035  pcmpt  13041  ennnfoneleminc  13162  ennnfonelemkh  13163  ennnfonelemhf1o  13164  ennnfonelemhom  13166  nninfdclemlt  13202  setsn0fun  13249  insubm  13698  ghmghmrn  13980  srgpcomp  14134  ringrng  14180  gsumfzfsumlemm  14735  tg2  14925  hmeof1o  15174  tgioo  15419  dvmptfsum  15590  plycolemc  15623  perfectlem2  15868  gausslemma2dlem0i  15930  lgsquad2lem2  15955  2lgslem3  15974  2lgs  15977  2lgsoddprm  15986  umgrnloop  16111  usgredg2vlem2  16218  subgrprop  16254  wlkv  16321  wlkl1loop  16353  wlk1walkdom  16354  uspgr2wlkeqi  16362  wlkres  16374  umgrclwwlkge2  16397  clwwlknp  16412  clwwlkext2edg  16417  clwwlknun  16436  eupth2fi  16474  bdfind  16716  bj-nn0sucALT  16748  nninfsellemqall  16793