Theorem mtbii 718

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

Hypotheses

Ref	Expression
mtbii.min	⊢ ¬ ψ
mtbii.maj	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
mtbii	⊢ (φ → ¬ χ)

Proof of Theorem mtbii

Step	Hyp	Ref	Expression
1		mtbii.min	. 2 ⊢ ¬ ψ
2		mtbii.maj	. . 3 ⊢ (φ → (ψ ↔ χ))
3	2	biimprd 154	. 2 ⊢ (φ → (χ → ψ))
4	1, 3	mtoi 107	1 ⊢ (φ → ¬ χ)

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146

This theorem is referenced by:  ssnpss 2152  noel 2287  aceq6b 4752  nd3 4952  axunndlem1 4959  axregndlem1 4966  axregndlem2 4967  axregnd 4968  axacndlem5 4975  addnidpi 5040  indpi 5046  prodgt0 5821  lt2msq 5883  vcoprne 8194  avril1 8779

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain