ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mtbiri GIF 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  3046  sspsstr  3047  psssstr  3048  n0i  3226  axnul  3879  intexr  3901  intnexr  3902  iin0r  3919  ordtriexmidlem  4232  ordtriexmidlem2  4233  ordtri2or2exmidlem  4238  onsucelsucexmidlem  4241  sucprcreg  4258  preleq  4264  nn0eln0  4319  0nelelxp  4351  tfrlemisucaccv  5917  nndceq  6055  nndcel  6056  2dom  6263  snnen2oprc  6301  elni2  6384  ltsopi  6390  ltsonq  6468  renepnf  7044  renemnf  7045  lt0ne0d  7474  nnne0  7909  nn0ge2m1nn  8205  xrltnr  8659  pnfnlt  8666  nltmnf  8667  xrltnsym  8672  xrlttri3  8676  nltpnft  8688  ngtmnft  8689  xrrebnd  8690  fzpreddisj  8891  fzm1  8920  bj-intexr  9892  bj-intnexr  9893
  Copyright terms: Public domain W3C validator