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  4742  sotri  5183  relcoi1  5319  f0rn0  5587  f1ocnv  5652  tz6.12c  5725  funbrfv  5739  fnbrfvb  5741  fvmptss2  5780  elfvmptrab1  5801  oprabid  6117  eloprabga  6175  elovmporab  6289  elovmporab1w  6290  relmptopab  6291  unielxp  6408  f1o2ndf1  6464  cnvoprab  6470  ressuppss  6494  tfrlem1  6579  tfr1onlemaccex  6619  tfrcllemaccex  6632  ecopovtrn  6906  ecopovtrng  6909  findcard2d  7195  findcard2sd  7196  fidcenumlemr  7272  fsuppimp  7292  difinfsn  7441  nnnninfeq2  7470  ismkvnex  7496  cc3  7635  ltexnqi  7777  prcdnql  7852  prcunqu  7853  prnmaxl  7856  prnminu  7857  ltprordil  7957  1idprl  7958  1idpru  7959  ltexprlemm  7968  ltexprlemopu  7971  ltexprlemru  7980  recexgt0sr  8141  mulgt0sr  8146  ltrenn  8223  nnindnn  8261  nnind  9323  nnmulcl  9328  nnnegz  9652  supinfneg  10005  infsupneg  10006  ublbneg  10023  ixxssxr  10313  ixxssixx  10315  iccshftri  10408  iccshftli  10410  iccdili  10412  icccntri  10414  1fv  10557  fzo1fzo0n0  10606  elfzonlteqm1  10639  ssfzo12  10653  exbtwnzlemshrink  10694  flqeqceilz  10770  zmodidfzoimp  10806  modfzo0difsn  10847  frec2uzltd  10855  frec2uzrdg  10861  frecuzrdgg  10868  seq3clss  10923  seq3fveq2  10927  seqfveq2g  10929  seq3shft2  10933  seqshft2g  10934  monoord  10937  seq3split  10940  seqsplitg  10941  seq3caopr3  10943  seqcaopr3g  10944  seq3f1olemp  10967  seqf1oglem2a  10970  seqf1og  10973  seq3id2  10978  seq3homo  10979  seq3z  10980  seqhomog  10982  seqfeq4g  10983  ser3ge0  10988  exp3vallem  10992  modqexp  11119  fihashf1rn  11243  hashfzp1  11281  seq3coll  11310  swrdswrd  11493  pfxccatin12lem2a  11515  pfxccatin12  11521  swrdccat  11523  pfxccat3a  11526  swrdccatin1d  11531  swrdccatin2d  11532  cjre  11663  climeu  12081  climub  12129  fsum2d  12221  fsumabs  12251  fsumiun  12263  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  prodfap0  12331  prodfrecap  12332  ntrivcvgap  12334  fprodabs  12402  fprod2d  12409  dvdsmod0  12579  p1modz1  12580  dvdsmodexp  12581  dvdsabseq  12633  mulsucdiv2z  12671  nno  12692  nn0o  12693  dfgcd2  12810  lcmgcdlem  12874  cncongr2  12901  exprmfct  12936  pwbdvdslemn  12963  eulerthlemrprm  13030  eulerthlema  13031  dvdsprmpweqnn  13138  dvdsprmpweqle  13139  pcmpt  13145  prmlem1a  13244  ballotfilemfc0  13284  ennnfoneleminc  13354  ennnfonelemkh  13355  ennnfonelemhf1o  13356  ennnfonelemhom  13358  nninfdclemlt  13394  setsn0fun  13441  insubm  13845  ghmghmrn  14119  srgpcomp  14378  ringrng  14425  tg2  15252  hmeof1o  15501  tgioo  15746  dvmptfsum  15917  plycolemc  15950  perfectlem2  16261  bposlem5  16276  gausslemma2dlem0i  16342  lgsquad2lem2  16367  2lgslem3  16386  2lgs  16389  2lgsoddprm  16398  umgrnloop  16523  usgredg2vlem2  16630  subgrprop  16666  wlkv  16733  wlkl1loop  16765  wlk1walkdom  16766  uspgr2wlkeqi  16774  wlkres  16786  umgrclwwlkge2  16809  clwwlknp  16824  clwwlkext2edg  16829  clwwlknun  16848  eupth2fi  16886  bdfind  17138  bj-nn0sucALT  17170  nninfsellemqall  17224