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

Theorem mtbiri 600
 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 590 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  3049  sspsstr  3050  psssstr  3051  n0i  3229  axnul  3882  intexr  3904  intnexr  3905  iin0r  3922  ordtriexmidlem  4245  ordtriexmidlem2  4246  ordtri2or2exmidlem  4251  onsucelsucexmidlem  4254  sucprcreg  4273  preleq  4279  reg3exmidlemwe  4303  nn0eln0  4341  0nelelxp  4373  tfrlemisucaccv  5939  nndceq  6077  nndcel  6078  2dom  6285  snnen2oprc  6323  elni2  6412  ltsopi  6418  ltsonq  6496  renepnf  7073  renemnf  7074  lt0ne0d  7505  nnne0  7942  nn0ge2m1nn  8242  xrltnr  8701  pnfnlt  8708  nltmnf  8709  xrltnsym  8714  xrlttri3  8718  nltpnft  8730  ngtmnft  8731  xrrebnd  8732  fzpreddisj  8933  fzm1  8962  bj-intexr  10028  bj-intnexr  10029
 Copyright terms: Public domain W3C validator