Theorem mtbid 678

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  682  eqneltrrd  2328  neleqtrd  2329  eueq3dc  2980  efrirr  4450  fidcenumlemrks  7151  nqnq0pi  7657  zdclt  9556  xleaddadd  10121  qdclt  10504  frec2uzf1od  10667  expnegap0  10808  bcval5  11024  zfz1isolemiso  11102  seq3coll  11105  fisumss  11952  fprodssdc  12150  nninfctlemfo  12610  rpdvds  12670  oddpwdclemodd  12743  pceq0  12894  pcmpt  12915  gsumfzval  13473  ply1termlem  15465  lgseisenlem1  15798  lgsquadlem3  15807  2sqlem8a  15850  2sqlem8  15851  2omap  16594  pwle2  16599