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  1735  ceqex  2665  peano2  4261  sotri  4663  relcoi1  4792  f1ocnv  5082  tz6.12c  5146  funbrfv  5155  fnbrfvb  5157  fvmptss2  5190  oprabid  5480  eloprabga  5533  unielxp  5742  f1o2ndf1  5791  tfrlem1  5864  freccl  5932  ecopovtrn  6139  ecopovtrng  6142  ltexnqi  6392  prcdnql  6466  prcunqu  6467  prnmaxl  6470  prnminu  6471  ltprordil  6564  1idprl  6565  1idpru  6566  ltexprlemm  6573  ltexprlemopu  6576  ltexprlemru  6585  recexgt0sr  6681  mulgt0sr  6684  nnind  7691  nnmulcl  7696  nnnegz  8004  ublbneg  8304  ixxssxr  8519  ixxssixx  8521  iccshftri  8613  iccshftli  8615  iccdili  8617  icccntri  8619  1fv  8746  fzo1fzo0n0  8789  elfzonlteqm1  8816  ssfzo12  8830  frec2uzltd  8850  frec2uzrdg  8856  iseqfveq2  8885  cjre  9090  bdfind  9380  bj-nn0sucALT  9408
  Copyright terms: Public domain W3C validator