Theorem mtbid 672

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 663	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 614  ax-in2 615

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnib  676  eqneltrrd  2274  neleqtrd  2275  eueq3dc  2911  efrirr  4353  fidcenumlemrks  6951  nqnq0pi  7436  zdclt  9329  xleaddadd  9886  frec2uzf1od  10405  expnegap0  10527  bcval5  10742  zfz1isolemiso  10818  seq3coll  10821  fisumss  11399  fprodssdc  11597  rpdvds  12098  oddpwdclemodd  12171  pceq0  12320  pcmpt  12340  lgseisenlem1  14420  2sqlem8a  14439  2sqlem8  14440  pwle2  14718