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

Theorem mtbiri 633
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 142 . 2 (𝜑 → (𝜓𝜒))
41, 3mtoi 623 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-in1 577  ax-in2 578
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  n0i  3280  axnul  3941  intexr  3963  intnexr  3964  iin0r  3981  exmid01  4008  ordtriexmidlem  4311  ordtriexmidlem2  4312  ordtri2or2exmidlem  4317  onsucelsucexmidlem  4320  sucprcreg  4340  preleq  4346  reg3exmidlemwe  4369  dcextest  4371  nn0eln0  4408  0nelelxp  4441  tfrlemisucaccv  6046  nnsucuniel  6212  nndceq  6216  nndcel  6217  2dom  6476  snnen2oprc  6530  snexxph  6611  djune  6716  updjudhcoinrg  6719  exmidfodomrlemrALT  6776  elni2  6820  ltsopi  6826  ltsonq  6904  renepnf  7482  renemnf  7483  lt0ne0d  7935  nnne0  8388  nn0ge2m1nn  8669  nn0nepnf  8680  xrltnr  9185  pnfnlt  9192  nltmnf  9193  xrltnsym  9198  xrlttri3  9202  nltpnft  9214  ngtmnft  9215  xrrebnd  9216  fzpreddisj  9418  fzm1  9447  exfzdc  9582  m1exp1  10807  3prm  11016  bj-intexr  11268  bj-intnexr  11269  nninfalllemn  11367  nninfsellemeq  11375  exmidsbthrlem  11381
  Copyright terms: Public domain W3C validator