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  2866  sbcn1  3012  sbcim1  3013  sbcbi1  3014  sbcel21v  3029  peano2  4596  sotri  5026  relcoi1  5162  f0rn0  5412  f1ocnv  5476  tz6.12c  5547  funbrfv  5556  fnbrfvb  5558  fvmptss2  5593  elfvmptrab1  5612  oprabid  5909  eloprabga  5964  unielxp  6177  f1o2ndf1  6231  cnvoprab  6237  tfrlem1  6311  tfr1onlemaccex  6351  tfrcllemaccex  6364  ecopovtrn  6634  ecopovtrng  6637  findcard2d  6893  findcard2sd  6894  fidcenumlemr  6956  difinfsn  7101  nnnninfeq2  7129  ismkvnex  7155  cc3  7269  ltexnqi  7410  prcdnql  7485  prcunqu  7486  prnmaxl  7489  prnminu  7490  ltprordil  7590  1idprl  7591  1idpru  7592  ltexprlemm  7601  ltexprlemopu  7604  ltexprlemru  7613  recexgt0sr  7774  mulgt0sr  7779  ltrenn  7856  nnindnn  7894  nnind  8937  nnmulcl  8942  nnnegz  9258  supinfneg  9597  infsupneg  9598  ublbneg  9615  ixxssxr  9902  ixxssixx  9904  iccshftri  9997  iccshftli  9999  iccdili  10001  icccntri  10003  1fv  10141  fzo1fzo0n0  10185  elfzonlteqm1  10212  ssfzo12  10226  exbtwnzlemshrink  10251  flqeqceilz  10320  zmodidfzoimp  10356  modfzo0difsn  10397  frec2uzltd  10405  frec2uzrdg  10411  frecuzrdgg  10418  seq3clss  10469  seq3fveq2  10471  seq3shft2  10475  monoord  10478  seq3split  10481  seq3caopr3  10483  seq3f1olemp  10504  seq3id2  10511  seq3homo  10512  seq3z  10513  ser3ge0  10519  exp3vallem  10523  modqexp  10649  fihashf1rn  10770  hashfzp1  10806  seq3coll  10824  cjre  10893  climeu  11306  climub  11354  fsum2d  11445  fsumabs  11475  fsumiun  11487  cvgratnnlemnexp  11534  cvgratnnlemmn  11535  prodfap0  11555  prodfrecap  11556  ntrivcvgap  11558  fprodabs  11626  fprod2d  11633  dvdsmod0  11802  p1modz1  11803  dvdsmodexp  11804  dvdsabseq  11855  mulsucdiv2z  11892  nno  11913  nn0o  11914  dfgcd2  12017  lcmgcdlem  12079  cncongr2  12106  exprmfct  12140  eulerthlemrprm  12231  eulerthlema  12232  dvdsprmpweqnn  12337  dvdsprmpweqle  12338  pcmpt  12343  ennnfoneleminc  12414  ennnfonelemkh  12415  ennnfonelemhf1o  12416  ennnfonelemhom  12418  nninfdclemlt  12454  setsn0fun  12501  insubm  12877  srgpcomp  13178  tg2  13599  hmeof1o  13848  tgioo  14085  bdfind  14737  bj-nn0sucALT  14769  nninfsellemqall  14803