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-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  syldan  270  ax16i  1754  ceqex  2694  sbcn1  2833  sbcim1  2834  sbcbi1  2835  sbcel21v  2850  peano2  4346  sotri  4748  relcoi1  4877  f1ocnv  5167  tz6.12c  5231  funbrfv  5240  fnbrfvb  5242  fvmptss2  5275  oprabid  5565  eloprabga  5619  unielxp  5828  f1o2ndf1  5877  cnvoprab  5883  tfrlem1  5954  freccl  6024  ecopovtrn  6234  ecopovtrng  6237  findcard2d  6379  findcard2sd  6380  ltexnqi  6565  prcdnql  6640  prcunqu  6641  prnmaxl  6644  prnminu  6645  ltprordil  6745  1idprl  6746  1idpru  6747  ltexprlemm  6756  ltexprlemopu  6759  ltexprlemru  6768  recexgt0sr  6916  mulgt0sr  6920  ltrenn  6989  nnindnn  7025  nnind  8006  nnmulcl  8011  nnnegz  8305  ublbneg  8645  ixxssxr  8870  ixxssixx  8872  iccshftri  8964  iccshftli  8966  iccdili  8968  icccntri  8970  1fv  9098  fzo1fzo0n0  9141  elfzonlteqm1  9168  ssfzo12  9182  flqeqceilz  9268  zmodidfzoimp  9304  modfzo0difsn  9345  frec2uzltd  9353  frec2uzrdg  9359  iseqfveq2  9392  iseqshft2  9396  monoord  9399  iseqsplit  9402  iseqcaopr3  9404  iseqhomo  9412  iseqz  9413  cjre  9710  climeu  10048  climub  10095  dvdsabseq  10159  mulsucdiv2z  10197  nno  10218  nn0o  10219  bdfind  10458  bj-nn0sucALT  10490
  Copyright terms: Public domain W3C validator