Theorem mtbid 632

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  sylnib  636  eqneltrrd  2184  neleqtrd  2185  eueq3dc  2789  efrirr  4180  fidcenumlemrks  6662  nqnq0pi  6997  zdclt  8824  frec2uzf1od  9813  expnegap0  9963  ibcval5  10171  zfz1isolemiso  10244  iseqcoll  10247  fisumss  10784  rpdvds  11359  oddpwdclemodd  11428