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

Step	Hyp	Ref	Expression
1		mtbiri.min	. 2 ⊢ ¬ χ
2		mtbiri.maj	. . 3 ⊢ (φ → (ψ ↔ χ))
3	2	biimpd 198	. 2 ⊢ (φ → (ψ → χ))
4	1, 3	mtoi 169	1 ⊢ (φ → ¬ ψ)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  psstr  3374  n0i  3556  pw10  4162  0nelsuc  4401  ltfinirr  4458  peano4  4558  addccan2  4560  phi011lem1  4599  ndmfvrcl  5351  xpnedisj  5514  oprssdm  5613  ndmovrcl  5617  ncssfin  6152  ncspw1eu  6160  nntccl  6171  ceclb  6184  ce0ncpw1  6186  cecl  6187  nclecid  6198  le0nc  6201  addlecncs  6210  nnc3n3p1  6279