Theorem mtbid 667

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylnib  671  eqneltrrd  2267  neleqtrd  2268  eueq3dc  2904  efrirr  4336  fidcenumlemrks  6927  nqnq0pi  7389  zdclt  9278  xleaddadd  9833  frec2uzf1od  10351  expnegap0  10473  bcval5  10686  zfz1isolemiso  10763  seq3coll  10766  fisumss  11344  fprodssdc  11542  rpdvds  12042  oddpwdclemodd  12115  pceq0  12264  pcmpt  12284  2sqlem8a  13713  2sqlem8  13714  pwle2  13993