Theorem mtbi 166

Description: An inference from a biconditional, related to modus tollens.

Hypotheses

Ref	Expression
mtbi.1	⊢ ¬ φ
mtbi.2	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
mtbi	⊢ ¬ ψ

Proof of Theorem mtbi

Step	Hyp	Ref	Expression
1		mtbi.1	. 2 ⊢ ¬ φ
2		mtbi.2	. . 3 ⊢ (φ ↔ ψ)
3	2	negbii 162	. 2 ⊢ (¬ φ ↔ ¬ ψ)
4	1, 3	mpbi 164	1 ⊢ ¬ ψ

Syntax hints:  ¬ wn 1   ↔ wb 127

This theorem is referenced by:  nvelv 1483  0nep0 1887  opprc1b 1906  opthwiener 1914  dmsnsn0 2544  karden 3551  alephprc 3698  cdacomen 3724

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

This theorem depends on definitions:  df-bi 128

metamath.org