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  2977  efrirr  4444  fidcenumlemrks  7120  nqnq0pi  7625  zdclt  9524  xleaddadd  10083  qdclt  10465  frec2uzf1od  10628  expnegap0  10769  bcval5  10985  zfz1isolemiso  11061  seq3coll  11064  fisumss  11903  fprodssdc  12101  nninfctlemfo  12561  rpdvds  12621  oddpwdclemodd  12694  pceq0  12845  pcmpt  12866  gsumfzval  13424  ply1termlem  15416  lgseisenlem1  15749  lgsquadlem3  15758  2sqlem8a  15801  2sqlem8  15802  2omap  16359  pwle2  16364