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

Theorem mtbir 606
Description: An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 14-Oct-2012.)
Hypotheses
Ref Expression
mtbir.1 ¬ 𝜓
mtbir.2 (𝜑𝜓)
Assertion
Ref Expression
mtbir ¬ 𝜑

Proof of Theorem mtbir
StepHypRef Expression
1 mtbir.1 . 2 ¬ 𝜓
2 mtbir.2 . . 3 (𝜑𝜓)
32bicomi 127 . 2 (𝜓𝜑)
41, 3mtbi 605 1 ¬ 𝜑
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  fal  1266  ax-9  1440  nonconne  2232  nemtbir  2309  ru  2785  pssirr  3071  noel  3255  npss0  3293  iun0  3740  0iun  3741  vprc  3915  iin0r  3949  nlim0  4158  snnex  4208  onsucelsucexmid  4282  0nelxp  4399  dm0  4576  iprc  4627  co02  4861  0fv  5235  frec0g  6013  0nnq  6519  0npr  6638  nqprdisj  6699  0ncn  6965  axpre-ltirr  7013  pnfnre  7125  mnfnre  7126  inelr  7648  xrltnr  8801  fzo0  9125  fzouzdisj  9137  sqrt2irr  10230  nnexmid  10265  nndc  10266  bj-vprc  10382
  Copyright terms: Public domain W3C validator