Theorem mtbid 679

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 158	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	mtod 669	1 ⊢ (𝜑 → ¬ 𝜒)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnib  683  eqneltrrd  2331  neleqtrd  2332  eueq3dc  2994  efrirr  4479  fidcenumlemrks  7236  2omap  7282  nqnq0pi  7769  zdclt  9672  xleaddadd  10239  qdclt  10629  frec2uzf1od  10792  expnegap0  10933  bcval5  11150  zfz1isolemiso  11236  seq3coll  11239  fisumss  12103  fprodssdc  12301  nninfctlemfo  12761  rpdvds  12821  oddpwdclemodd  12894  pceq0  13045  pcmpt  13066  gsumfzval  13654  ply1termlem  15733  lgseisenlem1  16069  lgsquadlem3  16078  2sqlem8a  16121  2sqlem8  16122  pwle2  16898