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  1869  ceqex  2888  sbcn1  3034  sbcim1  3035  sbcbi1  3036  sbcel21v  3051  ifnetruedc  3599  peano2  4628  sotri  5062  relcoi1  5198  f0rn0  5449  f1ocnv  5514  tz6.12c  5585  funbrfv  5596  fnbrfvb  5598  fvmptss2  5633  elfvmptrab1  5653  oprabid  5951  eloprabga  6006  elovmporab  6120  elovmporab1w  6121  unielxp  6229  f1o2ndf1  6283  cnvoprab  6289  tfrlem1  6363  tfr1onlemaccex  6403  tfrcllemaccex  6416  ecopovtrn  6688  ecopovtrng  6691  findcard2d  6949  findcard2sd  6950  fidcenumlemr  7016  difinfsn  7161  nnnninfeq2  7190  ismkvnex  7216  cc3  7330  ltexnqi  7471  prcdnql  7546  prcunqu  7547  prnmaxl  7550  prnminu  7551  ltprordil  7651  1idprl  7652  1idpru  7653  ltexprlemm  7662  ltexprlemopu  7665  ltexprlemru  7674  recexgt0sr  7835  mulgt0sr  7840  ltrenn  7917  nnindnn  7955  nnind  9000  nnmulcl  9005  nnnegz  9323  supinfneg  9663  infsupneg  9664  ublbneg  9681  ixxssxr  9969  ixxssixx  9971  iccshftri  10064  iccshftli  10066  iccdili  10068  icccntri  10070  1fv  10208  fzo1fzo0n0  10253  elfzonlteqm1  10280  ssfzo12  10294  exbtwnzlemshrink  10320  flqeqceilz  10392  zmodidfzoimp  10428  modfzo0difsn  10469  frec2uzltd  10477  frec2uzrdg  10483  frecuzrdgg  10490  seq3clss  10545  seq3fveq2  10549  seqfveq2g  10551  seq3shft2  10555  seqshft2g  10556  monoord  10559  seq3split  10562  seqsplitg  10563  seq3caopr3  10565  seqcaopr3g  10566  seq3f1olemp  10589  seqf1oglem2a  10592  seqf1og  10595  seq3id2  10600  seq3homo  10601  seq3z  10602  seqhomog  10604  seqfeq4g  10605  ser3ge0  10610  exp3vallem  10614  modqexp  10740  fihashf1rn  10862  hashfzp1  10898  seq3coll  10916  cjre  11029  climeu  11442  climub  11490  fsum2d  11581  fsumabs  11611  fsumiun  11623  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  prodfap0  11691  prodfrecap  11692  ntrivcvgap  11694  fprodabs  11762  fprod2d  11769  dvdsmod0  11939  p1modz1  11940  dvdsmodexp  11941  dvdsabseq  11992  mulsucdiv2z  12029  nno  12050  nn0o  12051  dfgcd2  12154  lcmgcdlem  12218  cncongr2  12245  exprmfct  12279  eulerthlemrprm  12370  eulerthlema  12371  dvdsprmpweqnn  12477  dvdsprmpweqle  12478  pcmpt  12484  ennnfoneleminc  12571  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ennnfonelemhom  12575  nninfdclemlt  12611  setsn0fun  12658  insubm  13060  ghmghmrn  13336  srgpcomp  13489  ringrng  13535  gsumfzfsumlemm  14086  tg2  14239  hmeof1o  14488  tgioo  14733  dvmptfsum  14904  plycolemc  14936  gausslemma2dlem0i  15214  lgsquad2lem2  15239  2lgslem3  15258  2lgs  15261  2lgsoddprm  15270  bdfind  15508  bj-nn0sucALT  15540  nninfsellemqall  15575