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 )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syldan  282  ax16i  1911  ceqex  2953  sbcn1  3099  sbcim1  3100  sbcbi1  3101  sbcel21v  3116  ifnetruedc  3684  peano2  4744  sotri  5186  relcoi1  5322  f0rn0  5590  f1ocnv  5655  tz6.12c  5728  funbrfv  5742  fnbrfvb  5744  fvmptss2  5783  elfvmptrab1  5804  oprabid  6120  eloprabga  6178  elovmporab  6292  elovmporab1w  6293  relmptopab  6294  unielxp  6412  f1o2ndf1  6468  cnvoprab  6474  ressuppss  6498  tfrlem1  6583  tfr1onlemaccex  6623  tfrcllemaccex  6636  ecopovtrn  6910  ecopovtrng  6913  findcard2d  7199  findcard2sd  7200  fidcenumlemr  7277  fsuppimp  7297  difinfsn  7446  nnnninfeq2  7475  ismkvnex  7501  cc3  7640  ltexnqi  7782  prcdnql  7857  prcunqu  7858  prnmaxl  7861  prnminu  7862  ltprordil  7962  1idprl  7963  1idpru  7964  ltexprlemm  7973  ltexprlemopu  7976  ltexprlemru  7985  recexgt0sr  8146  mulgt0sr  8151  ltrenn  8228  nnindnn  8266  nnind  9329  nnmulcl  9334  nnnegz  9658  supinfneg  10011  infsupneg  10012  ublbneg  10029  ixxssxr  10319  ixxssixx  10321  iccshftri  10414  iccshftli  10416  iccdili  10418  icccntri  10420  1fv  10563  fzo1fzo0n0  10612  elfzonlteqm1  10645  ssfzo12  10659  exbtwnzlemshrink  10700  flqeqceilz  10776  zmodidfzoimp  10812  modfzo0difsn  10853  frec2uzltd  10861  frec2uzrdg  10867  frecuzrdgg  10874  seq3clss  10929  seq3fveq2  10933  seqfveq2g  10935  seq3shft2  10939  seqshft2g  10940  monoord  10943  seq3split  10946  seqsplitg  10947  seq3caopr3  10949  seqcaopr3g  10950  seq3f1olemp  10973  seqf1oglem2a  10976  seqf1og  10979  seq3id2  10984  seq3homo  10985  seq3z  10986  seqhomog  10988  seqfeq4g  10989  ser3ge0  10994  exp3vallem  10998  modqexp  11125  fihashf1rn  11249  hashfzp1  11287  seq3coll  11316  swrdswrd  11499  pfxccatin12lem2a  11521  pfxccatin12  11527  swrdccat  11529  pfxccat3a  11532  swrdccatin1d  11537  swrdccatin2d  11538  cjre  11669  climeu  12087  climub  12135  fsum2d  12227  fsumabs  12257  fsumiun  12269  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  prodfap0  12337  prodfrecap  12338  ntrivcvgap  12340  fprodabs  12408  fprod2d  12415  dvdsmod0  12585  p1modz1  12586  dvdsmodexp  12587  dvdsabseq  12639  mulsucdiv2z  12677  nno  12698  nn0o  12699  dfgcd2  12816  lcmgcdlem  12880  cncongr2  12907  exprmfct  12942  pwbdvdslemn  12969  eulerthlemrprm  13036  eulerthlema  13037  dvdsprmpweqnn  13144  dvdsprmpweqle  13145  pcmpt  13151  prmlem1a  13250  ballotfilemfc0  13290  ennnfoneleminc  13360  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ennnfonelemhom  13364  nninfdclemlt  13400  setsn0fun  13447  insubm  13851  ghmghmrn  14125  srgpcomp  14401  ringrng  14448  tg2  15286  hmeof1o  15535  tgioo  15780  dvmptfsum  15951  plycolemc  15984  perfectlem2  16300  bposlem5  16315  gausslemma2dlem0i  16381  lgsquad2lem2  16406  2lgslem3  16425  2lgs  16428  2lgsoddprm  16437  umgrnloop  16562  usgredg2vlem2  16669  subgrprop  16705  wlkv  16772  wlkl1loop  16804  wlk1walkdom  16805  uspgr2wlkeqi  16813  wlkres  16825  umgrclwwlkge2  16848  clwwlknp  16863  clwwlkext2edg  16868  clwwlknun  16887  eupth2fi  16925  bdfind  17177  bj-nn0sucALT  17209  nninfsellemqall  17264