Theorem mtbid 676

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 667	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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnib  680  eqneltrrd  2326  neleqtrd  2327  eueq3dc  2978  efrirr  4448  fidcenumlemrks  7143  nqnq0pi  7648  zdclt  9547  xleaddadd  10112  qdclt  10495  frec2uzf1od  10658  expnegap0  10799  bcval5  11015  zfz1isolemiso  11093  seq3coll  11096  fisumss  11943  fprodssdc  12141  nninfctlemfo  12601  rpdvds  12661  oddpwdclemodd  12734  pceq0  12885  pcmpt  12906  gsumfzval  13464  ply1termlem  15456  lgseisenlem1  15789  lgsquadlem3  15798  2sqlem8a  15841  2sqlem8  15842  2omap  16530  pwle2  16535