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

Theorem mtbiri 610
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 136 . 2 (𝜑 → (𝜓𝜒))
41, 3mtoi 600 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-in1 554  ax-in2 555
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  psstr  3077  sspsstr  3078  psssstr  3079  n0i  3257  axnul  3910  intexr  3932  intnexr  3933  iin0r  3950  ordtriexmidlem  4273  ordtriexmidlem2  4274  ordtri2or2exmidlem  4279  onsucelsucexmidlem  4282  sucprcreg  4301  preleq  4307  reg3exmidlemwe  4331  nn0eln0  4369  0nelelxp  4401  tfrlemisucaccv  5970  nndceq  6108  nndcel  6109  2dom  6316  snnen2oprc  6354  elni2  6470  ltsopi  6476  ltsonq  6554  renepnf  7132  renemnf  7133  lt0ne0d  7579  nnne0  8018  nn0ge2m1nn  8299  xrltnr  8802  pnfnlt  8809  nltmnf  8810  xrltnsym  8815  xrlttri3  8819  nltpnft  8831  ngtmnft  8832  xrrebnd  8833  fzpreddisj  9035  fzm1  9064  m1exp1  10213  bj-intexr  10415  bj-intnexr  10416
  Copyright terms: Public domain W3C validator