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  1858  ceqex  2864  sbcn1  3010  sbcim1  3011  sbcbi1  3012  sbcel21v  3027  peano2  4594  sotri  5024  relcoi1  5160  f0rn0  5410  f1ocnv  5474  tz6.12c  5545  funbrfv  5554  fnbrfvb  5556  fvmptss2  5591  elfvmptrab1  5610  oprabid  5906  eloprabga  5961  unielxp  6174  f1o2ndf1  6228  cnvoprab  6234  tfrlem1  6308  tfr1onlemaccex  6348  tfrcllemaccex  6361  ecopovtrn  6631  ecopovtrng  6634  findcard2d  6890  findcard2sd  6891  fidcenumlemr  6953  difinfsn  7098  nnnninfeq2  7126  ismkvnex  7152  cc3  7266  ltexnqi  7407  prcdnql  7482  prcunqu  7483  prnmaxl  7486  prnminu  7487  ltprordil  7587  1idprl  7588  1idpru  7589  ltexprlemm  7598  ltexprlemopu  7601  ltexprlemru  7610  recexgt0sr  7771  mulgt0sr  7776  ltrenn  7853  nnindnn  7891  nnind  8934  nnmulcl  8939  nnnegz  9255  supinfneg  9594  infsupneg  9595  ublbneg  9612  ixxssxr  9899  ixxssixx  9901  iccshftri  9994  iccshftli  9996  iccdili  9998  icccntri  10000  1fv  10138  fzo1fzo0n0  10182  elfzonlteqm1  10209  ssfzo12  10223  exbtwnzlemshrink  10248  flqeqceilz  10317  zmodidfzoimp  10353  modfzo0difsn  10394  frec2uzltd  10402  frec2uzrdg  10408  frecuzrdgg  10415  seq3clss  10466  seq3fveq2  10468  seq3shft2  10472  monoord  10475  seq3split  10478  seq3caopr3  10480  seq3f1olemp  10501  seq3id2  10508  seq3homo  10509  seq3z  10510  ser3ge0  10516  exp3vallem  10520  modqexp  10646  fihashf1rn  10767  hashfzp1  10803  seq3coll  10821  cjre  10890  climeu  11303  climub  11351  fsum2d  11442  fsumabs  11472  fsumiun  11484  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  prodfap0  11552  prodfrecap  11553  ntrivcvgap  11555  fprodabs  11623  fprod2d  11630  dvdsmod0  11799  p1modz1  11800  dvdsmodexp  11801  dvdsabseq  11852  mulsucdiv2z  11889  nno  11910  nn0o  11911  dfgcd2  12014  lcmgcdlem  12076  cncongr2  12103  exprmfct  12137  eulerthlemrprm  12228  eulerthlema  12229  dvdsprmpweqnn  12334  dvdsprmpweqle  12335  pcmpt  12340  ennnfoneleminc  12411  ennnfonelemkh  12412  ennnfonelemhf1o  12413  ennnfonelemhom  12415  nninfdclemlt  12451  setsn0fun  12498  insubm  12871  srgpcomp  13171  tg2  13530  hmeof1o  13779  tgioo  14016  bdfind  14668  bj-nn0sucALT  14700  nninfsellemqall  14734