Theorem mtbid 667

Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.)

Hypotheses

Ref	Expression
mtbid.min	⊢ (𝜑 → ¬ 𝜓)
mtbid.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mtbid	⊢ (𝜑 → ¬ 𝜒)

Proof of Theorem mtbid

Step	Hyp	Ref	Expression
1		mtbid.min	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		mtbid.maj	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	biimprd 157	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	mtod 658	1 ⊢ (𝜑 → ¬ 𝜒)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylnib  671  eqneltrrd  2267  neleqtrd  2268  eueq3dc  2904  efrirr  4338  fidcenumlemrks  6930  nqnq0pi  7400  zdclt  9289  xleaddadd  9844  frec2uzf1od  10362  expnegap0  10484  bcval5  10697  zfz1isolemiso  10774  seq3coll  10777  fisumss  11355  fprodssdc  11553  rpdvds  12053  oddpwdclemodd  12126  pceq0  12275  pcmpt  12295  2sqlem8a  13752  2sqlem8  13753  pwle2  14031