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  1911  ceqex  2953  sbcn1  3099  sbcim1  3100  sbcbi1  3101  sbcel21v  3116  ifnetruedc  3681  peano2  4737  sotri  5178  relcoi1  5314  f0rn0  5582  f1ocnv  5647  tz6.12c  5720  funbrfv  5733  fnbrfvb  5735  fvmptss2  5774  elfvmptrab1  5794  oprabid  6107  eloprabga  6165  elovmporab  6279  elovmporab1w  6280  relmptopab  6281  unielxp  6398  f1o2ndf1  6454  cnvoprab  6460  ressuppss  6484  tfrlem1  6569  tfr1onlemaccex  6609  tfrcllemaccex  6622  ecopovtrn  6896  ecopovtrng  6899  findcard2d  7185  findcard2sd  7186  fidcenumlemr  7262  fsuppimp  7282  difinfsn  7430  nnnninfeq2  7459  ismkvnex  7485  cc3  7624  ltexnqi  7766  prcdnql  7841  prcunqu  7842  prnmaxl  7845  prnminu  7846  ltprordil  7946  1idprl  7947  1idpru  7948  ltexprlemm  7957  ltexprlemopu  7960  ltexprlemru  7969  recexgt0sr  8130  mulgt0sr  8135  ltrenn  8212  nnindnn  8250  nnind  9299  nnmulcl  9304  nnnegz  9626  supinfneg  9974  infsupneg  9975  ublbneg  9992  ixxssxr  10281  ixxssixx  10283  iccshftri  10376  iccshftli  10378  iccdili  10380  icccntri  10382  1fv  10524  fzo1fzo0n0  10573  elfzonlteqm1  10606  ssfzo12  10620  exbtwnzlemshrink  10661  flqeqceilz  10733  zmodidfzoimp  10769  modfzo0difsn  10810  frec2uzltd  10818  frec2uzrdg  10824  frecuzrdgg  10831  seq3clss  10886  seq3fveq2  10890  seqfveq2g  10892  seq3shft2  10896  seqshft2g  10897  monoord  10900  seq3split  10903  seqsplitg  10904  seq3caopr3  10906  seqcaopr3g  10907  seq3f1olemp  10930  seqf1oglem2a  10933  seqf1og  10936  seq3id2  10941  seq3homo  10942  seq3z  10943  seqhomog  10945  seqfeq4g  10946  ser3ge0  10951  exp3vallem  10955  modqexp  11082  fihashf1rn  11205  hashfzp1  11243  seq3coll  11272  swrdswrd  11455  pfxccatin12lem2a  11477  pfxccatin12  11483  swrdccat  11485  pfxccat3a  11488  swrdccatin1d  11493  swrdccatin2d  11494  cjre  11625  climeu  12040  climub  12088  fsum2d  12180  fsumabs  12210  fsumiun  12222  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  prodfap0  12290  prodfrecap  12291  ntrivcvgap  12293  fprodabs  12361  fprod2d  12368  dvdsmod0  12538  p1modz1  12539  dvdsmodexp  12540  dvdsabseq  12592  mulsucdiv2z  12630  nno  12651  nn0o  12652  dfgcd2  12769  lcmgcdlem  12833  cncongr2  12860  exprmfct  12894  eulerthlemrprm  12985  eulerthlema  12986  dvdsprmpweqnn  13093  dvdsprmpweqle  13094  pcmpt  13100  ballotfilemfc0  13210  ennnfoneleminc  13280  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ennnfonelemhom  13284  nninfdclemlt  13320  setsn0fun  13367  insubm  13769  ghmghmrn  14043  srgpcomp  14268  ringrng  14314  tg2  15084  hmeof1o  15333  tgioo  15578  dvmptfsum  15749  plycolemc  15782  perfectlem2  16028  gausslemma2dlem0i  16090  lgsquad2lem2  16115  2lgslem3  16134  2lgs  16137  2lgsoddprm  16146  umgrnloop  16271  usgredg2vlem2  16378  subgrprop  16414  wlkv  16481  wlkl1loop  16513  wlk1walkdom  16514  uspgr2wlkeqi  16522  wlkres  16534  umgrclwwlkge2  16557  clwwlknp  16572  clwwlkext2edg  16577  clwwlknun  16596  eupth2fi  16634  bdfind  16886  bj-nn0sucALT  16918  nninfsellemqall  16963