ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpcom Unicode version

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
StepHypRef Expression
1 mpcom.1 . 2  |-  ( ps 
->  ph )
2 mpcom.2 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
32com12 30 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
41, 3mpd 13 1  |-  ( ps 
->  ch )
Colors of variables: wff set class
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  cc3  7083  ltexnqi  7224  prcdnql  7299  prcunqu  7300  prnmaxl  7303  prnminu  7304  ltprordil  7404  1idprl  7405  1idpru  7406  ltexprlemm  7415  ltexprlemopu  7418  ltexprlemru  7427  recexgt0sr  7588  mulgt0sr  7593  ltrenn  7670  nnindnn  7708  nnind  8743  nnmulcl  8748  nnnegz  9064  supinfneg  9397  infsupneg  9398  ublbneg  9412  ixxssxr  9690  ixxssixx  9692  iccshftri  9785  iccshftli  9787  iccdili  9789  icccntri  9791  1fv  9923  fzo1fzo0n0  9967  elfzonlteqm1  9994  ssfzo12  10008  exbtwnzlemshrink  10033  flqeqceilz  10098  zmodidfzoimp  10134  modfzo0difsn  10175  frec2uzltd  10183  frec2uzrdg  10189  frecuzrdgg  10196  seq3clss  10247  seq3fveq2  10249  seq3shft2  10253  monoord  10256  seq3split  10259  seq3caopr3  10261  seq3f1olemp  10282  seq3id2  10289  seq3homo  10290  seq3z  10291  ser3ge0  10297  exp3vallem  10301  fihashf1rn  10542  hashfzp1  10577  seq3coll  10592  cjre  10661  climeu  11072  climub  11120  fsum2d  11211  fsumabs  11241  fsumiun  11253  cvgratnnlemnexp  11300  cvgratnnlemmn  11301  prodfap0  11321  prodfrecap  11322  ntrivcvgap  11324  dvdsabseq  11552  mulsucdiv2z  11589  nno  11610  nn0o  11611  dfgcd2  11709  lcmgcdlem  11765  cncongr2  11792  exprmfct  11825  ennnfoneleminc  11931  ennnfonelemkh  11932  ennnfonelemhf1o  11933  ennnfonelemhom  11935  setsn0fun  12006  tg2  12239  hmeof1o  12488  tgioo  12725  bdfind  13174  bj-nn0sucALT  13206  nninfsellemqall  13241
  Copyright terms: Public domain W3C validator