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  2934  sbcn1  3080  sbcim1  3081  sbcbi1  3082  sbcel21v  3097  ifnetruedc  3653  peano2  4699  sotri  5139  relcoi1  5275  f0rn0  5540  f1ocnv  5605  tz6.12c  5678  funbrfv  5691  fnbrfvb  5693  fvmptss2  5730  elfvmptrab1  5750  oprabid  6060  eloprabga  6118  elovmporab  6232  elovmporab1w  6233  relmptopab  6234  unielxp  6346  f1o2ndf1  6402  cnvoprab  6408  ressuppss  6432  tfrlem1  6517  tfr1onlemaccex  6557  tfrcllemaccex  6570  ecopovtrn  6844  ecopovtrng  6847  findcard2d  7123  findcard2sd  7124  fidcenumlemr  7197  difinfsn  7342  nnnninfeq2  7371  ismkvnex  7397  cc3  7530  ltexnqi  7672  prcdnql  7747  prcunqu  7748  prnmaxl  7751  prnminu  7752  ltprordil  7852  1idprl  7853  1idpru  7854  ltexprlemm  7863  ltexprlemopu  7866  ltexprlemru  7875  recexgt0sr  8036  mulgt0sr  8041  ltrenn  8118  nnindnn  8156  nnind  9201  nnmulcl  9206  nnnegz  9526  supinfneg  9873  infsupneg  9874  ublbneg  9891  ixxssxr  10179  ixxssixx  10181  iccshftri  10274  iccshftli  10276  iccdili  10278  icccntri  10280  1fv  10419  fzo1fzo0n0  10468  elfzonlteqm1  10501  ssfzo12  10515  exbtwnzlemshrink  10554  flqeqceilz  10626  zmodidfzoimp  10662  modfzo0difsn  10703  frec2uzltd  10711  frec2uzrdg  10717  frecuzrdgg  10724  seq3clss  10779  seq3fveq2  10783  seqfveq2g  10785  seq3shft2  10789  seqshft2g  10790  monoord  10793  seq3split  10796  seqsplitg  10797  seq3caopr3  10799  seqcaopr3g  10800  seq3f1olemp  10823  seqf1oglem2a  10826  seqf1og  10829  seq3id2  10834  seq3homo  10835  seq3z  10836  seqhomog  10838  seqfeq4g  10839  ser3ge0  10844  exp3vallem  10848  modqexp  10974  fihashf1rn  11096  hashfzp1  11134  seq3coll  11152  swrdswrd  11335  pfxccatin12lem2a  11357  pfxccatin12  11363  swrdccat  11365  pfxccat3a  11368  swrdccatin1d  11373  swrdccatin2d  11374  cjre  11505  climeu  11919  climub  11967  fsum2d  12059  fsumabs  12089  fsumiun  12101  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  prodfap0  12169  prodfrecap  12170  ntrivcvgap  12172  fprodabs  12240  fprod2d  12247  dvdsmod0  12417  p1modz1  12418  dvdsmodexp  12419  dvdsabseq  12471  mulsucdiv2z  12509  nno  12530  nn0o  12531  dfgcd2  12648  lcmgcdlem  12712  cncongr2  12739  exprmfct  12773  eulerthlemrprm  12864  eulerthlema  12865  dvdsprmpweqnn  12972  dvdsprmpweqle  12973  pcmpt  12979  ennnfoneleminc  13095  ennnfonelemkh  13096  ennnfonelemhf1o  13097  ennnfonelemhom  13099  nninfdclemlt  13135  setsn0fun  13182  insubm  13631  ghmghmrn  13913  srgpcomp  14067  ringrng  14113  gsumfzfsumlemm  14666  tg2  14854  hmeof1o  15103  tgioo  15348  dvmptfsum  15519  plycolemc  15552  perfectlem2  15797  gausslemma2dlem0i  15859  lgsquad2lem2  15884  2lgslem3  15903  2lgs  15906  2lgsoddprm  15915  umgrnloop  16040  usgredg2vlem2  16147  subgrprop  16183  wlkv  16250  wlkl1loop  16282  wlk1walkdom  16283  uspgr2wlkeqi  16291  wlkres  16303  umgrclwwlkge2  16326  clwwlknp  16341  clwwlkext2edg  16346  clwwlknun  16365  eupth2fi  16403  bdfind  16645  bj-nn0sucALT  16677  nninfsellemqall  16724