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

Theorem mpcom 32
Description: Modus ponens inference with commutation of antecedents. (Contributed by NM, 17-Mar-1996.)
Hypotheses
Ref Expression
mpcom.1 (ψφ)
mpcom.2 (φ → (ψχ))
Assertion
Ref Expression
mpcom (ψχ)

Proof of Theorem mpcom
StepHypRef Expression
1 mpcom.1 . 2 (ψφ)
2 mpcom.2 . . 3 (φ → (ψχ))
32com12 27 . 2 (ψ → (φχ))
41, 3mpd 13 1 (ψχ)
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  266  ax16i  1720  ceqex  2648  peano2  4245  sotri  4647  relcoi1  4776  f1ocnv  5064  tz6.12c  5128  funbrfv  5137  fnbrfvb  5139  fvmptss2  5172  oprabid  5461  eloprabga  5514  unielxp  5723  f1o2ndf1  5772  tfrlem1  5845  ecopovtrn  6114  ecopovtrng  6117  prcdnql  6338  prcunqu  6339  prnmaxl  6342  prnminu  6343  prmuloc  6410  ltprordil  6428  1idprl  6429  1idpru  6430  ltexprlemm  6437  ltexprlemopu  6440  ltexprlemloc  6444  ltexprlemru  6449  addcanprlemu  6452  recexsrlem  6520  mulgt0sr  6522  bdfind  7168  bj-nn0sucALT  7196
  Copyright terms: Public domain W3C validator