New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  mtbir GIF version

Theorem mtbir 290
 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 193 . 2 (ψφ)
41, 3mtbi 289 1 ¬ φ
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 176 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177 This theorem is referenced by:  fal  1322  nonconne  2523  nemtbir  2604  ru  3045  pssirr  3369  indifdir  3511  necompl  3544  noel  3554  npss0  3589  iun0  4022  0iun  4023  0nel1c  4159  0nelsuc  4400  nndisjeq  4429  addcnul1  4452  eqtfinrelk  4486  nulnnn  4556  0cnelphi  4597  dm0  4918  cnv0  5031  co02  5092  co01  5093  nfunv  5138  imadif  5171  fv01  5354  1p1e2c  6155  2p1e3c  6156  fnfreclem2  6318
 Copyright terms: Public domain W3C validator