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  4592  sotri  5021  relcoi1  5157  f0rn0  5407  f1ocnv  5471  tz6.12c  5542  funbrfv  5551  fnbrfvb  5553  fvmptss2  5588  elfvmptrab1  5607  oprabid  5902  eloprabga  5957  unielxp  6170  f1o2ndf1  6224  cnvoprab  6230  tfrlem1  6304  tfr1onlemaccex  6344  tfrcllemaccex  6357  ecopovtrn  6627  ecopovtrng  6630  findcard2d  6886  findcard2sd  6887  fidcenumlemr  6949  difinfsn  7094  nnnninfeq2  7122  ismkvnex  7148  cc3  7262  ltexnqi  7403  prcdnql  7478  prcunqu  7479  prnmaxl  7482  prnminu  7483  ltprordil  7583  1idprl  7584  1idpru  7585  ltexprlemm  7594  ltexprlemopu  7597  ltexprlemru  7606  recexgt0sr  7767  mulgt0sr  7772  ltrenn  7849  nnindnn  7887  nnind  8929  nnmulcl  8934  nnnegz  9250  supinfneg  9589  infsupneg  9590  ublbneg  9607  ixxssxr  9894  ixxssixx  9896  iccshftri  9989  iccshftli  9991  iccdili  9993  icccntri  9995  1fv  10132  fzo1fzo0n0  10176  elfzonlteqm1  10203  ssfzo12  10217  exbtwnzlemshrink  10242  flqeqceilz  10311  zmodidfzoimp  10347  modfzo0difsn  10388  frec2uzltd  10396  frec2uzrdg  10402  frecuzrdgg  10409  seq3clss  10460  seq3fveq2  10462  seq3shft2  10466  monoord  10469  seq3split  10472  seq3caopr3  10474  seq3f1olemp  10495  seq3id2  10502  seq3homo  10503  seq3z  10504  ser3ge0  10510  exp3vallem  10514  modqexp  10639  fihashf1rn  10759  hashfzp1  10795  seq3coll  10813  cjre  10882  climeu  11295  climub  11343  fsum2d  11434  fsumabs  11464  fsumiun  11476  cvgratnnlemnexp  11523  cvgratnnlemmn  11524  prodfap0  11544  prodfrecap  11545  ntrivcvgap  11547  fprodabs  11615  fprod2d  11622  dvdsmod0  11791  p1modz1  11792  dvdsmodexp  11793  dvdsabseq  11843  mulsucdiv2z  11880  nno  11901  nn0o  11902  dfgcd2  12005  lcmgcdlem  12067  cncongr2  12094  exprmfct  12128  eulerthlemrprm  12219  eulerthlema  12220  dvdsprmpweqnn  12325  dvdsprmpweqle  12326  pcmpt  12331  ennnfoneleminc  12402  ennnfonelemkh  12403  ennnfonelemhf1o  12404  ennnfonelemhom  12406  nninfdclemlt  12442  setsn0fun  12489  insubm  12800  srgpcomp  13073  tg2  13342  hmeof1o  13591  tgioo  13828  bdfind  14469  bj-nn0sucALT  14501  nninfsellemqall  14535