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  6563  1idprl  6564  1idpru  6565  ltexprlemm  6572  ltexprlemopu  6575  ltexprlemru  6584  recexgt0sr  6661  mulgt0sr  6664  nnind  7671  nnmulcl  7676  nnnegz  7984  ublbneg  8284  ixxssxr  8499  ixxssixx  8501  iccshftri  8593  iccshftli  8595  iccdili  8597  icccntri  8599  1fv  8726  fzo1fzo0n0  8769  elfzonlteqm1  8796  ssfzo12  8810  frec2uzltd  8830  frec2uzrdg  8836  iseqfveq2  8865  cjre  9070  bdfind  9334  bj-nn0sucALT  9362
  Copyright terms: Public domain W3C validator