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

Theorem mtbiri 294
 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 198 . 2 (φ → (ψχ))
41, 3mtoi 169 1 (φ → ¬ ψ)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ 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:  psstr  3373  n0i  3555  pw10  4161  0nelsuc  4400  ltfinirr  4457  peano4  4557  addccan2  4559  phi011lem1  4598  ndmfvrcl  5350  xpnedisj  5513  oprssdm  5612  ndmovrcl  5616  ncssfin  6151  ncspw1eu  6159  nntccl  6170  ceclb  6183  ce0ncpw1  6185  cecl  6186  nclecid  6197  le0nc  6200  addlecncs  6209  nnc3n3p1  6278
 Copyright terms: Public domain W3C validator