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  1872  ceqex  2891  sbcn1  3037  sbcim1  3038  sbcbi1  3039  sbcel21v  3054  ifnetruedc  3603  peano2  4632  sotri  5066  relcoi1  5202  f0rn0  5455  f1ocnv  5520  tz6.12c  5591  funbrfv  5602  fnbrfvb  5604  fvmptss2  5639  elfvmptrab1  5659  oprabid  5957  eloprabga  6013  elovmporab  6127  elovmporab1w  6128  unielxp  6241  f1o2ndf1  6295  cnvoprab  6301  tfrlem1  6375  tfr1onlemaccex  6415  tfrcllemaccex  6428  ecopovtrn  6700  ecopovtrng  6703  findcard2d  6961  findcard2sd  6962  fidcenumlemr  7030  difinfsn  7175  nnnninfeq2  7204  ismkvnex  7230  cc3  7351  ltexnqi  7493  prcdnql  7568  prcunqu  7569  prnmaxl  7572  prnminu  7573  ltprordil  7673  1idprl  7674  1idpru  7675  ltexprlemm  7684  ltexprlemopu  7687  ltexprlemru  7696  recexgt0sr  7857  mulgt0sr  7862  ltrenn  7939  nnindnn  7977  nnind  9023  nnmulcl  9028  nnnegz  9346  supinfneg  9686  infsupneg  9687  ublbneg  9704  ixxssxr  9992  ixxssixx  9994  iccshftri  10087  iccshftli  10089  iccdili  10091  icccntri  10093  1fv  10231  fzo1fzo0n0  10276  elfzonlteqm1  10303  ssfzo12  10317  exbtwnzlemshrink  10355  flqeqceilz  10427  zmodidfzoimp  10463  modfzo0difsn  10504  frec2uzltd  10512  frec2uzrdg  10518  frecuzrdgg  10525  seq3clss  10580  seq3fveq2  10584  seqfveq2g  10586  seq3shft2  10590  seqshft2g  10591  monoord  10594  seq3split  10597  seqsplitg  10598  seq3caopr3  10600  seqcaopr3g  10601  seq3f1olemp  10624  seqf1oglem2a  10627  seqf1og  10630  seq3id2  10635  seq3homo  10636  seq3z  10637  seqhomog  10639  seqfeq4g  10640  ser3ge0  10645  exp3vallem  10649  modqexp  10775  fihashf1rn  10897  hashfzp1  10933  seq3coll  10951  cjre  11064  climeu  11478  climub  11526  fsum2d  11617  fsumabs  11647  fsumiun  11659  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  prodfap0  11727  prodfrecap  11728  ntrivcvgap  11730  fprodabs  11798  fprod2d  11805  dvdsmod0  11975  p1modz1  11976  dvdsmodexp  11977  dvdsabseq  12029  mulsucdiv2z  12067  nno  12088  nn0o  12089  dfgcd2  12206  lcmgcdlem  12270  cncongr2  12297  exprmfct  12331  eulerthlemrprm  12422  eulerthlema  12423  dvdsprmpweqnn  12530  dvdsprmpweqle  12531  pcmpt  12537  ennnfoneleminc  12653  ennnfonelemkh  12654  ennnfonelemhf1o  12655  ennnfonelemhom  12657  nninfdclemlt  12693  setsn0fun  12740  insubm  13187  ghmghmrn  13469  srgpcomp  13622  ringrng  13668  gsumfzfsumlemm  14219  tg2  14380  hmeof1o  14629  tgioo  14874  dvmptfsum  15045  plycolemc  15078  perfectlem2  15320  gausslemma2dlem0i  15382  lgsquad2lem2  15407  2lgslem3  15426  2lgs  15429  2lgsoddprm  15438  bdfind  15676  bj-nn0sucALT  15708  nninfsellemqall  15746