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  280  ax16i  1846  ceqex  2852  sbcn1  2997  sbcim1  2998  sbcbi1  2999  sbcel21v  3014  peano2  4571  sotri  4998  relcoi1  5134  f0rn0  5381  f1ocnv  5444  tz6.12c  5515  funbrfv  5524  fnbrfvb  5526  fvmptss2  5560  elfvmptrab1  5579  oprabid  5870  eloprabga  5925  unielxp  6139  f1o2ndf1  6192  cnvoprab  6198  tfrlem1  6272  tfr1onlemaccex  6312  tfrcllemaccex  6325  ecopovtrn  6594  ecopovtrng  6597  findcard2d  6853  findcard2sd  6854  fidcenumlemr  6916  difinfsn  7061  nnnninfeq2  7089  ismkvnex  7115  cc3  7205  ltexnqi  7346  prcdnql  7421  prcunqu  7422  prnmaxl  7425  prnminu  7426  ltprordil  7526  1idprl  7527  1idpru  7528  ltexprlemm  7537  ltexprlemopu  7540  ltexprlemru  7549  recexgt0sr  7710  mulgt0sr  7715  ltrenn  7792  nnindnn  7830  nnind  8869  nnmulcl  8874  nnnegz  9190  supinfneg  9529  infsupneg  9530  ublbneg  9547  ixxssxr  9832  ixxssixx  9834  iccshftri  9927  iccshftli  9929  iccdili  9931  icccntri  9933  1fv  10070  fzo1fzo0n0  10114  elfzonlteqm1  10141  ssfzo12  10155  exbtwnzlemshrink  10180  flqeqceilz  10249  zmodidfzoimp  10285  modfzo0difsn  10326  frec2uzltd  10334  frec2uzrdg  10340  frecuzrdgg  10347  seq3clss  10398  seq3fveq2  10400  seq3shft2  10404  monoord  10407  seq3split  10410  seq3caopr3  10412  seq3f1olemp  10433  seq3id2  10440  seq3homo  10441  seq3z  10442  ser3ge0  10448  exp3vallem  10452  modqexp  10577  fihashf1rn  10698  hashfzp1  10733  seq3coll  10751  cjre  10820  climeu  11233  climub  11281  fsum2d  11372  fsumabs  11402  fsumiun  11414  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  prodfap0  11482  prodfrecap  11483  ntrivcvgap  11485  fprodabs  11553  fprod2d  11560  dvdsmod0  11729  p1modz1  11730  dvdsmodexp  11731  dvdsabseq  11781  mulsucdiv2z  11818  nno  11839  nn0o  11840  dfgcd2  11943  lcmgcdlem  12005  cncongr2  12032  exprmfct  12066  eulerthlemrprm  12157  eulerthlema  12158  dvdsprmpweqnn  12263  dvdsprmpweqle  12264  pcmpt  12269  ennnfoneleminc  12340  ennnfonelemkh  12341  ennnfonelemhf1o  12342  ennnfonelemhom  12344  nninfdclemlt  12380  setsn0fun  12427  tg2  12660  hmeof1o  12909  tgioo  13146  bdfind  13788  bj-nn0sucALT  13820  nninfsellemqall  13855