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 )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syldan  282  ax16i  1911  ceqex  2953  sbcn1  3099  sbcim1  3100  sbcbi1  3101  sbcel21v  3116  ifnetruedc  3684  peano2  4742  sotri  5183  relcoi1  5319  f0rn0  5587  f1ocnv  5652  tz6.12c  5725  funbrfv  5739  fnbrfvb  5741  fvmptss2  5780  elfvmptrab1  5801  oprabid  6117  eloprabga  6175  elovmporab  6289  elovmporab1w  6290  relmptopab  6291  unielxp  6408  f1o2ndf1  6464  cnvoprab  6470  ressuppss  6494  tfrlem1  6579  tfr1onlemaccex  6619  tfrcllemaccex  6632  ecopovtrn  6906  ecopovtrng  6909  findcard2d  7195  findcard2sd  7196  fidcenumlemr  7272  fsuppimp  7292  difinfsn  7440  nnnninfeq2  7469  ismkvnex  7495  cc3  7634  ltexnqi  7776  prcdnql  7851  prcunqu  7852  prnmaxl  7855  prnminu  7856  ltprordil  7956  1idprl  7957  1idpru  7958  ltexprlemm  7967  ltexprlemopu  7970  ltexprlemru  7979  recexgt0sr  8140  mulgt0sr  8145  ltrenn  8222  nnindnn  8260  nnind  9322  nnmulcl  9327  nnnegz  9651  supinfneg  10004  infsupneg  10005  ublbneg  10022  ixxssxr  10312  ixxssixx  10314  iccshftri  10407  iccshftli  10409  iccdili  10411  icccntri  10413  1fv  10556  fzo1fzo0n0  10605  elfzonlteqm1  10638  ssfzo12  10652  exbtwnzlemshrink  10693  flqeqceilz  10768  zmodidfzoimp  10804  modfzo0difsn  10845  frec2uzltd  10853  frec2uzrdg  10859  frecuzrdgg  10866  seq3clss  10921  seq3fveq2  10925  seqfveq2g  10927  seq3shft2  10931  seqshft2g  10932  monoord  10935  seq3split  10938  seqsplitg  10939  seq3caopr3  10941  seqcaopr3g  10942  seq3f1olemp  10965  seqf1oglem2a  10968  seqf1og  10971  seq3id2  10976  seq3homo  10977  seq3z  10978  seqhomog  10980  seqfeq4g  10981  ser3ge0  10986  exp3vallem  10990  modqexp  11117  fihashf1rn  11241  hashfzp1  11279  seq3coll  11308  swrdswrd  11491  pfxccatin12lem2a  11513  pfxccatin12  11519  swrdccat  11521  pfxccat3a  11524  swrdccatin1d  11529  swrdccatin2d  11530  cjre  11661  climeu  12078  climub  12126  fsum2d  12218  fsumabs  12248  fsumiun  12260  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  prodfap0  12328  prodfrecap  12329  ntrivcvgap  12331  fprodabs  12399  fprod2d  12406  dvdsmod0  12576  p1modz1  12577  dvdsmodexp  12578  dvdsabseq  12630  mulsucdiv2z  12668  nno  12689  nn0o  12690  dfgcd2  12807  lcmgcdlem  12871  cncongr2  12898  exprmfct  12933  pwbdvdslemn  12960  eulerthlemrprm  13027  eulerthlema  13028  dvdsprmpweqnn  13135  dvdsprmpweqle  13136  pcmpt  13142  prmlem1a  13241  ballotfilemfc0  13281  ennnfoneleminc  13351  ennnfonelemkh  13352  ennnfonelemhf1o  13353  ennnfonelemhom  13355  nninfdclemlt  13391  setsn0fun  13438  insubm  13841  ghmghmrn  14115  srgpcomp  14343  ringrng  14390  tg2  15210  hmeof1o  15459  tgioo  15704  dvmptfsum  15875  plycolemc  15908  perfectlem2  16198  bposlem5  16213  gausslemma2dlem0i  16274  lgsquad2lem2  16299  2lgslem3  16318  2lgs  16321  2lgsoddprm  16330  umgrnloop  16455  usgredg2vlem2  16562  subgrprop  16598  wlkv  16665  wlkl1loop  16697  wlk1walkdom  16698  uspgr2wlkeqi  16706  wlkres  16718  umgrclwwlkge2  16741  clwwlknp  16756  clwwlkext2edg  16761  clwwlknun  16780  eupth2fi  16818  bdfind  17070  bj-nn0sucALT  17102  nninfsellemqall  17156