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 ⊢ (𝜑 → ¬ 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 105

This proof depends on 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 proof depends on definitions:  df-bi 117

This theorem is used by:  sylnib  687  eqneltrrd  2335  neleqtrd  2336  eueq3dc  3000  efrirr  4500  fidcenumlemrks  7275  2omap  7324  nqnq0pi  7811  zdclt  9733  xleaddadd  10306  qdclt  10697  frec2uzf1od  10864  expnegap0  11005  bcval5  11223  zfz1isolemiso  11313  seq3coll  11316  fisumss  12184  fprodssdc  12382  nninfctlemfo  12842  rpdvds  12902  nnmaxpwlemnfac  12976  pceq0  13130  pcmpt  13151  prmlem0  13249  gzsumfzval  13770  ply1termlem  15968  lgseisenlem1  16394  lgsquadlem3  16403  2sqlem8a  16446  2sqlem8  16447  pwle2  17233  stnot  17244  wexmiddifxylem  17250