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  6584  tfr1onlemaccex  6624  tfrcllemaccex  6637  ecopovtrn  6911  ecopovtrng  6914  findcard2d  7201  findcard2sd  7202  fidcenumlemr  7279  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  9656  supinfneg  10010  infsupneg  10011  ublbneg  10028  ixxssxr  10318  ixxssixx  10320  iccshftri  10413  iccshftli  10415  iccdili  10417  icccntri  10419  1fv  10562  fzo1fzo0n0  10611  elfzonlteqm1  10644  ssfzo12  10658  exbtwnzlemshrink  10699  flqeqceilz  10775  zmodidfzoimp  10811  modfzo0difsn  10852  frec2uzltd  10860  frec2uzrdg  10866  frecuzrdgg  10873  seq3clss  10928  seq3fveq2  10932  seqfveq2g  10934  seq3shft2  10938  seqshft2g  10939  monoord  10942  seq3split  10945  seqsplitg  10946  seq3caopr3  10948  seqcaopr3g  10949  seq3f1olemp  10972  seqf1oglem2a  10975  seqf1og  10978  seq3id2  10983  seq3homo  10984  seq3z  10985  seqhomog  10987  seqfeq4g  10988  ser3ge0  10993  exp3vallem  10997  modqexp  11124  fihashf1rn  11248  hashfzp1  11286  seq3coll  11315  swrdswrd  11498  pfxccatin12lem2a  11520  pfxccatin12  11526  swrdccat  11528  pfxccat3a  11531  swrdccatin1d  11536  swrdccatin2d  11537  cjre  11668  climeu  12086  climub  12134  fsum2d  12226  fsumabs  12256  fsumiun  12268  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  prodfap0  12336  prodfrecap  12337  ntrivcvgap  12339  fprodabs  12407  fprod2d  12414  dvdsmod0  12584  p1modz1  12585  dvdsmodexp  12586  dvdsabseq  12638  mulsucdiv2z  12676  nno  12697  nn0o  12698  dfgcd2  12815  lcmgcdlem  12879  cncongr2  12906  exprmfct  12941  pwbdvdslemn  12968  eulerthlemrprm  13035  eulerthlema  13036  dvdsprmpweqnn  13143  dvdsprmpweqle  13144  pcmpt  13150  prmlem1a  13249  ballotfilemfc0  13289  ennnfoneleminc  13359  ennnfonelemkh  13360  ennnfonelemhf1o  13361  ennnfonelemhom  13363  nninfdclemlt  13399  setsn0fun  13446  insubm  13850  ghmghmrn  14124  srgpcomp  14400  ringrng  14447  tg2  15303  hmeof1o  15552  tgioo  15797  dvmptfsum  15968  plycolemc  16001  perfectlem2  16317  bposlem5  16332  gausslemma2dlem0i  16398  lgsquad2lem2  16423  2lgslem3  16442  2lgs  16445  2lgsoddprm  16454  umgrnloop  16579  usgredg2vlem2  16686  subgrprop  16722  wlkv  16789  wlkl1loop  16821  wlk1walkdom  16822  uspgr2wlkeqi  16830  wlkres  16842  umgrclwwlkge2  16865  clwwlknp  16880  clwwlkext2edg  16885  clwwlknun  16904  eupth2fi  16942  bdfind  17194  bj-nn0sucALT  17226  nninfsellemqall  17281