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  1906  ceqex  2933  sbcn1  3079  sbcim1  3080  sbcbi1  3081  sbcel21v  3096  ifnetruedc  3649  peano2  4693  sotri  5132  relcoi1  5268  f0rn0  5531  f1ocnv  5596  tz6.12c  5669  funbrfv  5682  fnbrfvb  5684  fvmptss2  5721  elfvmptrab1  5741  oprabid  6050  eloprabga  6108  elovmporab  6222  elovmporab1w  6223  relmptopab  6224  unielxp  6337  f1o2ndf1  6393  cnvoprab  6399  tfrlem1  6474  tfr1onlemaccex  6514  tfrcllemaccex  6527  ecopovtrn  6801  ecopovtrng  6804  findcard2d  7080  findcard2sd  7081  fidcenumlemr  7154  difinfsn  7299  nnnninfeq2  7328  ismkvnex  7354  cc3  7487  ltexnqi  7629  prcdnql  7704  prcunqu  7705  prnmaxl  7708  prnminu  7709  ltprordil  7809  1idprl  7810  1idpru  7811  ltexprlemm  7820  ltexprlemopu  7823  ltexprlemru  7832  recexgt0sr  7993  mulgt0sr  7998  ltrenn  8075  nnindnn  8113  nnind  9159  nnmulcl  9164  nnnegz  9482  supinfneg  9829  infsupneg  9830  ublbneg  9847  ixxssxr  10135  ixxssixx  10137  iccshftri  10230  iccshftli  10232  iccdili  10234  icccntri  10236  1fv  10374  fzo1fzo0n0  10423  elfzonlteqm1  10456  ssfzo12  10470  exbtwnzlemshrink  10509  flqeqceilz  10581  zmodidfzoimp  10617  modfzo0difsn  10658  frec2uzltd  10666  frec2uzrdg  10672  frecuzrdgg  10679  seq3clss  10734  seq3fveq2  10738  seqfveq2g  10740  seq3shft2  10744  seqshft2g  10745  monoord  10748  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  seqcaopr3g  10755  seq3f1olemp  10778  seqf1oglem2a  10781  seqf1og  10784  seq3id2  10789  seq3homo  10790  seq3z  10791  seqhomog  10793  seqfeq4g  10794  ser3ge0  10799  exp3vallem  10803  modqexp  10929  fihashf1rn  11051  hashfzp1  11089  seq3coll  11107  swrdswrd  11290  pfxccatin12lem2a  11312  pfxccatin12  11318  swrdccat  11320  pfxccat3a  11323  swrdccatin1d  11328  swrdccatin2d  11329  cjre  11460  climeu  11874  climub  11922  fsum2d  12014  fsumabs  12044  fsumiun  12056  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  prodfap0  12124  prodfrecap  12125  ntrivcvgap  12127  fprodabs  12195  fprod2d  12202  dvdsmod0  12372  p1modz1  12373  dvdsmodexp  12374  dvdsabseq  12426  mulsucdiv2z  12464  nno  12485  nn0o  12486  dfgcd2  12603  lcmgcdlem  12667  cncongr2  12694  exprmfct  12728  eulerthlemrprm  12819  eulerthlema  12820  dvdsprmpweqnn  12927  dvdsprmpweqle  12928  pcmpt  12934  ennnfoneleminc  13050  ennnfonelemkh  13051  ennnfonelemhf1o  13052  ennnfonelemhom  13054  nninfdclemlt  13090  setsn0fun  13137  insubm  13586  ghmghmrn  13868  srgpcomp  14022  ringrng  14068  gsumfzfsumlemm  14620  tg2  14803  hmeof1o  15052  tgioo  15297  dvmptfsum  15468  plycolemc  15501  perfectlem2  15743  gausslemma2dlem0i  15805  lgsquad2lem2  15830  2lgslem3  15849  2lgs  15852  2lgsoddprm  15861  umgrnloop  15986  usgredg2vlem2  16093  subgrprop  16129  wlkv  16196  wlkl1loop  16228  wlk1walkdom  16229  uspgr2wlkeqi  16237  wlkres  16249  umgrclwwlkge2  16272  clwwlknp  16287  clwwlkext2edg  16292  clwwlknun  16311  eupth2fi  16349  bdfind  16592  bj-nn0sucALT  16624  nninfsellemqall  16668