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  1852  ceqex  2858  sbcn1  3003  sbcim1  3004  sbcbi1  3005  sbcel21v  3020  peano2  4580  sotri  5008  relcoi1  5144  f0rn0  5394  f1ocnv  5458  tz6.12c  5529  funbrfv  5538  fnbrfvb  5540  fvmptss2  5575  elfvmptrab1  5594  oprabid  5889  eloprabga  5944  unielxp  6157  f1o2ndf1  6211  cnvoprab  6217  tfrlem1  6291  tfr1onlemaccex  6331  tfrcllemaccex  6344  ecopovtrn  6614  ecopovtrng  6617  findcard2d  6873  findcard2sd  6874  fidcenumlemr  6936  difinfsn  7081  nnnninfeq2  7109  ismkvnex  7135  cc3  7234  ltexnqi  7375  prcdnql  7450  prcunqu  7451  prnmaxl  7454  prnminu  7455  ltprordil  7555  1idprl  7556  1idpru  7557  ltexprlemm  7566  ltexprlemopu  7569  ltexprlemru  7578  recexgt0sr  7739  mulgt0sr  7744  ltrenn  7821  nnindnn  7859  nnind  8898  nnmulcl  8903  nnnegz  9219  supinfneg  9558  infsupneg  9559  ublbneg  9576  ixxssxr  9861  ixxssixx  9863  iccshftri  9956  iccshftli  9958  iccdili  9960  icccntri  9962  1fv  10099  fzo1fzo0n0  10143  elfzonlteqm1  10170  ssfzo12  10184  exbtwnzlemshrink  10209  flqeqceilz  10278  zmodidfzoimp  10314  modfzo0difsn  10355  frec2uzltd  10363  frec2uzrdg  10369  frecuzrdgg  10376  seq3clss  10427  seq3fveq2  10429  seq3shft2  10433  monoord  10436  seq3split  10439  seq3caopr3  10441  seq3f1olemp  10462  seq3id2  10469  seq3homo  10470  seq3z  10471  ser3ge0  10477  exp3vallem  10481  modqexp  10606  fihashf1rn  10727  hashfzp1  10763  seq3coll  10781  cjre  10850  climeu  11263  climub  11311  fsum2d  11402  fsumabs  11432  fsumiun  11444  cvgratnnlemnexp  11491  cvgratnnlemmn  11492  prodfap0  11512  prodfrecap  11513  ntrivcvgap  11515  fprodabs  11583  fprod2d  11590  dvdsmod0  11759  p1modz1  11760  dvdsmodexp  11761  dvdsabseq  11811  mulsucdiv2z  11848  nno  11869  nn0o  11870  dfgcd2  11973  lcmgcdlem  12035  cncongr2  12062  exprmfct  12096  eulerthlemrprm  12187  eulerthlema  12188  dvdsprmpweqnn  12293  dvdsprmpweqle  12294  pcmpt  12299  ennnfoneleminc  12370  ennnfonelemkh  12371  ennnfonelemhf1o  12372  ennnfonelemhom  12374  nninfdclemlt  12410  setsn0fun  12457  insubm  12707  tg2  12939  hmeof1o  13188  tgioo  13425  bdfind  14066  bj-nn0sucALT  14098  nninfsellemqall  14133