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

Theorem mtbir 596
 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 123 . 2 (𝜓𝜑)
41, 3mtbi 595 1 ¬ 𝜑
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  fal  1250  ax-9  1424  nonconne  2217  nemtbir  2294  ru  2763  pssirr  3044  noel  3228  npss0  3266  iun0  3713  0iun  3714  vprc  3888  iin0r  3922  nlim0  4131  snnex  4181  onsucelsucexmid  4255  0nelxp  4372  dm0  4549  iprc  4600  co02  4834  0fv  5208  frec0g  5983  0nnq  6462  0npr  6581  nqprdisj  6642  0ncn  6908  axpre-ltirr  6956  pnfnre  7067  mnfnre  7068  inelr  7575  xrltnr  8701  fzo0  9024  fzouzdisj  9036  sqrt2irr  9878  nnexmid  9899  nndc  9900  bj-vprc  10016
 Copyright terms: Public domain W3C validator