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  1882  ceqex  2907  sbcn1  3053  sbcim1  3054  sbcbi1  3055  sbcel21v  3070  ifnetruedc  3623  peano2  4661  sotri  5097  relcoi1  5233  f0rn0  5492  f1ocnv  5557  tz6.12c  5629  funbrfv  5640  fnbrfvb  5642  fvmptss2  5677  elfvmptrab1  5697  oprabid  5999  eloprabga  6055  elovmporab  6169  elovmporab1w  6170  unielxp  6283  f1o2ndf1  6337  cnvoprab  6343  tfrlem1  6417  tfr1onlemaccex  6457  tfrcllemaccex  6470  ecopovtrn  6742  ecopovtrng  6745  findcard2d  7014  findcard2sd  7015  fidcenumlemr  7083  difinfsn  7228  nnnninfeq2  7257  ismkvnex  7283  cc3  7415  ltexnqi  7557  prcdnql  7632  prcunqu  7633  prnmaxl  7636  prnminu  7637  ltprordil  7737  1idprl  7738  1idpru  7739  ltexprlemm  7748  ltexprlemopu  7751  ltexprlemru  7760  recexgt0sr  7921  mulgt0sr  7926  ltrenn  8003  nnindnn  8041  nnind  9087  nnmulcl  9092  nnnegz  9410  supinfneg  9751  infsupneg  9752  ublbneg  9769  ixxssxr  10057  ixxssixx  10059  iccshftri  10152  iccshftli  10154  iccdili  10156  icccntri  10158  1fv  10296  fzo1fzo0n0  10344  elfzonlteqm1  10376  ssfzo12  10390  exbtwnzlemshrink  10428  flqeqceilz  10500  zmodidfzoimp  10536  modfzo0difsn  10577  frec2uzltd  10585  frec2uzrdg  10591  frecuzrdgg  10598  seq3clss  10653  seq3fveq2  10657  seqfveq2g  10659  seq3shft2  10663  seqshft2g  10664  monoord  10667  seq3split  10670  seqsplitg  10671  seq3caopr3  10673  seqcaopr3g  10674  seq3f1olemp  10697  seqf1oglem2a  10700  seqf1og  10703  seq3id2  10708  seq3homo  10709  seq3z  10710  seqhomog  10712  seqfeq4g  10713  ser3ge0  10718  exp3vallem  10722  modqexp  10848  fihashf1rn  10970  hashfzp1  11006  seq3coll  11024  swrdswrd  11196  pfxccatin12lem2a  11218  pfxccatin12  11224  swrdccat  11226  pfxccat3a  11229  swrdccatin1d  11234  swrdccatin2d  11235  cjre  11308  climeu  11722  climub  11770  fsum2d  11861  fsumabs  11891  fsumiun  11903  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  prodfap0  11971  prodfrecap  11972  ntrivcvgap  11974  fprodabs  12042  fprod2d  12049  dvdsmod0  12219  p1modz1  12220  dvdsmodexp  12221  dvdsabseq  12273  mulsucdiv2z  12311  nno  12332  nn0o  12333  dfgcd2  12450  lcmgcdlem  12514  cncongr2  12541  exprmfct  12575  eulerthlemrprm  12666  eulerthlema  12667  dvdsprmpweqnn  12774  dvdsprmpweqle  12775  pcmpt  12781  ennnfoneleminc  12897  ennnfonelemkh  12898  ennnfonelemhf1o  12899  ennnfonelemhom  12901  nninfdclemlt  12937  setsn0fun  12984  insubm  13432  ghmghmrn  13714  srgpcomp  13867  ringrng  13913  gsumfzfsumlemm  14464  tg2  14647  hmeof1o  14896  tgioo  15141  dvmptfsum  15312  plycolemc  15345  perfectlem2  15587  gausslemma2dlem0i  15649  lgsquad2lem2  15674  2lgslem3  15693  2lgs  15696  2lgsoddprm  15705  bdfind  16081  bj-nn0sucALT  16113  nninfsellemqall  16154