ILE Home 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  2215  nemtbir  2291  ru  2760  pssirr  3041  noel  3225  npss0  3263  iun0  3710  0iun  3711  vprc  3885  iin0r  3919  nlim0  4127  snnex  4177  onsucelsucexmid  4251  0nelxp  4359  dm0  4536  iprc  4587  co02  4821  0fv  5195  frec0g  5970  0nnq  6443  0npr  6562  nqprdisj  6623  0ncn  6889  axpre-ltirr  6937  pnfnre  7047  mnfnre  7048  inelr  7551  xrltnr  8668  fzo0  8991  fzouzdisj  9003  sqrt2irr  9755  nnexmid  9772  nndc  9773  bj-vprc  9889
  Copyright terms: Public domain W3C validator