ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mtbiri Unicode 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  6870  renemnf  6871  lt0ne0d  7300  nnne0  7723  nn0ge2m1nn  8018  xrltnr  8471  pnfnlt  8478  nltmnf  8479  xrltnsym  8484  xrlttri3  8488  nltpnft  8500  ngtmnft  8501  xrrebnd  8502  fzpreddisj  8703  fzm1  8732  bj-intexr  9363  bj-intnexr  9364
  Copyright terms: Public domain W3C validator