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  2931  sbcn1  3077  sbcim1  3078  sbcbi1  3079  sbcel21v  3094  ifnetruedc  3647  peano2  4691  sotri  5130  relcoi1  5266  f0rn0  5528  f1ocnv  5593  tz6.12c  5665  funbrfv  5678  fnbrfvb  5680  fvmptss2  5717  elfvmptrab1  5737  oprabid  6045  eloprabga  6103  elovmporab  6217  elovmporab1w  6218  relmptopab  6219  unielxp  6332  f1o2ndf1  6388  cnvoprab  6394  tfrlem1  6469  tfr1onlemaccex  6509  tfrcllemaccex  6522  ecopovtrn  6796  ecopovtrng  6799  findcard2d  7073  findcard2sd  7074  fidcenumlemr  7145  difinfsn  7290  nnnninfeq2  7319  ismkvnex  7345  cc3  7477  ltexnqi  7619  prcdnql  7694  prcunqu  7695  prnmaxl  7698  prnminu  7699  ltprordil  7799  1idprl  7800  1idpru  7801  ltexprlemm  7810  ltexprlemopu  7813  ltexprlemru  7822  recexgt0sr  7983  mulgt0sr  7988  ltrenn  8065  nnindnn  8103  nnind  9149  nnmulcl  9154  nnnegz  9472  supinfneg  9819  infsupneg  9820  ublbneg  9837  ixxssxr  10125  ixxssixx  10127  iccshftri  10220  iccshftli  10222  iccdili  10224  icccntri  10226  1fv  10364  fzo1fzo0n0  10412  elfzonlteqm1  10445  ssfzo12  10459  exbtwnzlemshrink  10498  flqeqceilz  10570  zmodidfzoimp  10606  modfzo0difsn  10647  frec2uzltd  10655  frec2uzrdg  10661  frecuzrdgg  10668  seq3clss  10723  seq3fveq2  10727  seqfveq2g  10729  seq3shft2  10733  seqshft2g  10734  monoord  10737  seq3split  10740  seqsplitg  10741  seq3caopr3  10743  seqcaopr3g  10744  seq3f1olemp  10767  seqf1oglem2a  10770  seqf1og  10773  seq3id2  10778  seq3homo  10779  seq3z  10780  seqhomog  10782  seqfeq4g  10783  ser3ge0  10788  exp3vallem  10792  modqexp  10918  fihashf1rn  11040  hashfzp1  11078  seq3coll  11096  swrdswrd  11276  pfxccatin12lem2a  11298  pfxccatin12  11304  swrdccat  11306  pfxccat3a  11309  swrdccatin1d  11314  swrdccatin2d  11315  cjre  11433  climeu  11847  climub  11895  fsum2d  11986  fsumabs  12016  fsumiun  12028  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  prodfap0  12096  prodfrecap  12097  ntrivcvgap  12099  fprodabs  12167  fprod2d  12174  dvdsmod0  12344  p1modz1  12345  dvdsmodexp  12346  dvdsabseq  12398  mulsucdiv2z  12436  nno  12457  nn0o  12458  dfgcd2  12575  lcmgcdlem  12639  cncongr2  12666  exprmfct  12700  eulerthlemrprm  12791  eulerthlema  12792  dvdsprmpweqnn  12899  dvdsprmpweqle  12900  pcmpt  12906  ennnfoneleminc  13022  ennnfonelemkh  13023  ennnfonelemhf1o  13024  ennnfonelemhom  13026  nninfdclemlt  13062  setsn0fun  13109  insubm  13558  ghmghmrn  13840  srgpcomp  13993  ringrng  14039  gsumfzfsumlemm  14591  tg2  14774  hmeof1o  15023  tgioo  15268  dvmptfsum  15439  plycolemc  15472  perfectlem2  15714  gausslemma2dlem0i  15776  lgsquad2lem2  15801  2lgslem3  15820  2lgs  15823  2lgsoddprm  15832  umgrnloop  15957  usgredg2vlem2  16062  wlkv  16123  wlkl1loop  16155  wlk1walkdom  16156  uspgr2wlkeqi  16164  wlkres  16174  umgrclwwlkge2  16197  clwwlknp  16212  clwwlkext2edg  16217  clwwlknun  16236  bdfind  16477  bj-nn0sucALT  16509  nninfsellemqall  16553