Theorem mtbid 683

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 673	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 623  ax-in2 624

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnib  687  eqneltrrd  2335  neleqtrd  2336  eueq3dc  3000  efrirr  4493  fidcenumlemrks  7260  2omap  7308  nqnq0pi  7795  zdclt  9701  xleaddadd  10268  qdclt  10658  frec2uzf1od  10821  expnegap0  10962  bcval5  11179  zfz1isolemiso  11269  seq3coll  11272  fisumss  12137  fprodssdc  12335  nninfctlemfo  12795  rpdvds  12855  oddpwdclemodd  12928  pceq0  13079  pcmpt  13100  gzsumfzval  13688  ply1termlem  15766  lgseisenlem1  16103  lgsquadlem3  16112  2sqlem8a  16155  2sqlem8  16156  pwle2  16942