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  280  ax16i  1830  ceqex  2812  sbcn1  2956  sbcim1  2957  sbcbi1  2958  sbcel21v  2973  peano2  4509  sotri  4934  relcoi1  5070  f0rn0  5317  f1ocnv  5380  tz6.12c  5451  funbrfv  5460  fnbrfvb  5462  fvmptss2  5496  elfvmptrab1  5515  oprabid  5803  eloprabga  5858  unielxp  6072  f1o2ndf1  6125  cnvoprab  6131  tfrlem1  6205  tfr1onlemaccex  6245  tfrcllemaccex  6258  ecopovtrn  6526  ecopovtrng  6529  findcard2d  6785  findcard2sd  6786  fidcenumlemr  6843  difinfsn  6985  ismkvnex  7029  ltexnqi  7217  prcdnql  7292  prcunqu  7293  prnmaxl  7296  prnminu  7297  ltprordil  7397  1idprl  7398  1idpru  7399  ltexprlemm  7408  ltexprlemopu  7411  ltexprlemru  7420  recexgt0sr  7581  mulgt0sr  7586  ltrenn  7663  nnindnn  7701  nnind  8736  nnmulcl  8741  nnnegz  9057  supinfneg  9390  infsupneg  9391  ublbneg  9405  ixxssxr  9683  ixxssixx  9685  iccshftri  9778  iccshftli  9780  iccdili  9782  icccntri  9784  1fv  9916  fzo1fzo0n0  9960  elfzonlteqm1  9987  ssfzo12  10001  exbtwnzlemshrink  10026  flqeqceilz  10091  zmodidfzoimp  10127  modfzo0difsn  10168  frec2uzltd  10176  frec2uzrdg  10182  frecuzrdgg  10189  seq3clss  10240  seq3fveq2  10242  seq3shft2  10246  monoord  10249  seq3split  10252  seq3caopr3  10254  seq3f1olemp  10275  seq3id2  10282  seq3homo  10283  seq3z  10284  ser3ge0  10290  exp3vallem  10294  fihashf1rn  10535  hashfzp1  10570  seq3coll  10585  cjre  10654  climeu  11065  climub  11113  fsum2d  11204  fsumabs  11234  fsumiun  11246  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  prodfap0  11314  prodfrecap  11315  ntrivcvgap  11317  dvdsabseq  11545  mulsucdiv2z  11582  nno  11603  nn0o  11604  dfgcd2  11702  lcmgcdlem  11758  cncongr2  11785  exprmfct  11818  ennnfoneleminc  11924  ennnfonelemkh  11925  ennnfonelemhf1o  11926  ennnfonelemhom  11928  setsn0fun  11996  tg2  12229  hmeof1o  12478  tgioo  12715  bdfind  13144  bj-nn0sucALT  13176  nninfsellemqall  13211