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  1904  ceqex  2930  sbcn1  3076  sbcim1  3077  sbcbi1  3078  sbcel21v  3093  ifnetruedc  3646  peano2  4686  sotri  5123  relcoi1  5259  f0rn0  5519  f1ocnv  5584  tz6.12c  5656  funbrfv  5669  fnbrfvb  5671  fvmptss2  5708  elfvmptrab1  5728  oprabid  6032  eloprabga  6090  elovmporab  6204  elovmporab1w  6205  unielxp  6318  f1o2ndf1  6372  cnvoprab  6378  tfrlem1  6452  tfr1onlemaccex  6492  tfrcllemaccex  6505  ecopovtrn  6777  ecopovtrng  6780  findcard2d  7049  findcard2sd  7050  fidcenumlemr  7118  difinfsn  7263  nnnninfeq2  7292  ismkvnex  7318  cc3  7450  ltexnqi  7592  prcdnql  7667  prcunqu  7668  prnmaxl  7671  prnminu  7672  ltprordil  7772  1idprl  7773  1idpru  7774  ltexprlemm  7783  ltexprlemopu  7786  ltexprlemru  7795  recexgt0sr  7956  mulgt0sr  7961  ltrenn  8038  nnindnn  8076  nnind  9122  nnmulcl  9127  nnnegz  9445  supinfneg  9786  infsupneg  9787  ublbneg  9804  ixxssxr  10092  ixxssixx  10094  iccshftri  10187  iccshftli  10189  iccdili  10191  icccntri  10193  1fv  10331  fzo1fzo0n0  10379  elfzonlteqm1  10411  ssfzo12  10425  exbtwnzlemshrink  10463  flqeqceilz  10535  zmodidfzoimp  10571  modfzo0difsn  10612  frec2uzltd  10620  frec2uzrdg  10626  frecuzrdgg  10633  seq3clss  10688  seq3fveq2  10692  seqfveq2g  10694  seq3shft2  10698  seqshft2g  10699  monoord  10702  seq3split  10705  seqsplitg  10706  seq3caopr3  10708  seqcaopr3g  10709  seq3f1olemp  10732  seqf1oglem2a  10735  seqf1og  10738  seq3id2  10743  seq3homo  10744  seq3z  10745  seqhomog  10747  seqfeq4g  10748  ser3ge0  10753  exp3vallem  10757  modqexp  10883  fihashf1rn  11005  hashfzp1  11041  seq3coll  11059  swrdswrd  11232  pfxccatin12lem2a  11254  pfxccatin12  11260  swrdccat  11262  pfxccat3a  11265  swrdccatin1d  11270  swrdccatin2d  11271  cjre  11388  climeu  11802  climub  11850  fsum2d  11941  fsumabs  11971  fsumiun  11983  cvgratnnlemnexp  12030  cvgratnnlemmn  12031  prodfap0  12051  prodfrecap  12052  ntrivcvgap  12054  fprodabs  12122  fprod2d  12129  dvdsmod0  12299  p1modz1  12300  dvdsmodexp  12301  dvdsabseq  12353  mulsucdiv2z  12391  nno  12412  nn0o  12413  dfgcd2  12530  lcmgcdlem  12594  cncongr2  12621  exprmfct  12655  eulerthlemrprm  12746  eulerthlema  12747  dvdsprmpweqnn  12854  dvdsprmpweqle  12855  pcmpt  12861  ennnfoneleminc  12977  ennnfonelemkh  12978  ennnfonelemhf1o  12979  ennnfonelemhom  12981  nninfdclemlt  13017  setsn0fun  13064  insubm  13513  ghmghmrn  13795  srgpcomp  13948  ringrng  13994  gsumfzfsumlemm  14545  tg2  14728  hmeof1o  14977  tgioo  15222  dvmptfsum  15393  plycolemc  15426  perfectlem2  15668  gausslemma2dlem0i  15730  lgsquad2lem2  15755  2lgslem3  15774  2lgs  15777  2lgsoddprm  15786  umgrnloop  15910  usgredg2vlem2  16015  bdfind  16267  bj-nn0sucALT  16299  nninfsellemqall  16340