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  1856  ceqex  2862  sbcn1  3008  sbcim1  3009  sbcbi1  3010  sbcel21v  3025  peano2  4588  sotri  5016  relcoi1  5152  f0rn0  5402  f1ocnv  5466  tz6.12c  5537  funbrfv  5546  fnbrfvb  5548  fvmptss2  5583  elfvmptrab1  5602  oprabid  5897  eloprabga  5952  unielxp  6165  f1o2ndf1  6219  cnvoprab  6225  tfrlem1  6299  tfr1onlemaccex  6339  tfrcllemaccex  6352  ecopovtrn  6622  ecopovtrng  6625  findcard2d  6881  findcard2sd  6882  fidcenumlemr  6944  difinfsn  7089  nnnninfeq2  7117  ismkvnex  7143  cc3  7242  ltexnqi  7383  prcdnql  7458  prcunqu  7459  prnmaxl  7462  prnminu  7463  ltprordil  7563  1idprl  7564  1idpru  7565  ltexprlemm  7574  ltexprlemopu  7577  ltexprlemru  7586  recexgt0sr  7747  mulgt0sr  7752  ltrenn  7829  nnindnn  7867  nnind  8906  nnmulcl  8911  nnnegz  9227  supinfneg  9566  infsupneg  9567  ublbneg  9584  ixxssxr  9869  ixxssixx  9871  iccshftri  9964  iccshftli  9966  iccdili  9968  icccntri  9970  1fv  10107  fzo1fzo0n0  10151  elfzonlteqm1  10178  ssfzo12  10192  exbtwnzlemshrink  10217  flqeqceilz  10286  zmodidfzoimp  10322  modfzo0difsn  10363  frec2uzltd  10371  frec2uzrdg  10377  frecuzrdgg  10384  seq3clss  10435  seq3fveq2  10437  seq3shft2  10441  monoord  10444  seq3split  10447  seq3caopr3  10449  seq3f1olemp  10470  seq3id2  10477  seq3homo  10478  seq3z  10479  ser3ge0  10485  exp3vallem  10489  modqexp  10614  fihashf1rn  10734  hashfzp1  10770  seq3coll  10788  cjre  10857  climeu  11270  climub  11318  fsum2d  11409  fsumabs  11439  fsumiun  11451  cvgratnnlemnexp  11498  cvgratnnlemmn  11499  prodfap0  11519  prodfrecap  11520  ntrivcvgap  11522  fprodabs  11590  fprod2d  11597  dvdsmod0  11766  p1modz1  11767  dvdsmodexp  11768  dvdsabseq  11818  mulsucdiv2z  11855  nno  11876  nn0o  11877  dfgcd2  11980  lcmgcdlem  12042  cncongr2  12069  exprmfct  12103  eulerthlemrprm  12194  eulerthlema  12195  dvdsprmpweqnn  12300  dvdsprmpweqle  12301  pcmpt  12306  ennnfoneleminc  12377  ennnfonelemkh  12378  ennnfonelemhf1o  12379  ennnfonelemhom  12381  nninfdclemlt  12417  setsn0fun  12464  insubm  12732  srgpcomp  12968  tg2  13129  hmeof1o  13378  tgioo  13615  bdfind  14256  bj-nn0sucALT  14288  nninfsellemqall  14323