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

Theorem mtbiri 599
Description: An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.)
Hypotheses
Ref Expression
mtbiri.min ¬ χ
mtbiri.maj (φ → (ψχ))
Assertion
Ref Expression
mtbiri (φ → ¬ ψ)

Proof of Theorem mtbiri
StepHypRef Expression
1 mtbiri.min . 2 ¬ χ
2 mtbiri.maj . . 3 (φ → (ψχ))
32biimpd 132 . 2 (φ → (ψχ))
41, 3mtoi 589 1 (φ → ¬ ψ)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-in1 544  ax-in2 545
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  psstr  3043  sspsstr  3044  psssstr  3045  n0i  3223  axnul  3873  intexr  3895  intnexr  3896  iin0r  3913  ordtriexmidlem  4208  ordtriexmidlem2  4209  onsucelsucexmidlem  4214  sucprcreg  4227  preleq  4233  nn0eln0  4284  0nelelxp  4316  tfrlemisucaccv  5880  nndceq  6015  nndcel  6016  2dom  6221  elni2  6298  ltsopi  6304  ltsonq  6382  renepnf  6850  renemnf  6851  lt0ne0d  7280  nnne0  7703  nn0ge2m1nn  7998  xrltnr  8451  pnfnlt  8458  nltmnf  8459  xrltnsym  8464  xrlttri3  8468  nltpnft  8480  ngtmnft  8481  xrrebnd  8482  fzpreddisj  8683  fzm1  8712  bj-intexr  9339  bj-intnexr  9340
  Copyright terms: Public domain W3C validator