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  4498  fidcenumlemrks  7270  2omap  7319  nqnq0pi  7806  zdclt  9727  xleaddadd  10300  qdclt  10691  frec2uzf1od  10858  expnegap0  10999  bcval5  11217  zfz1isolemiso  11307  seq3coll  11310  fisumss  12178  fprodssdc  12376  nninfctlemfo  12836  rpdvds  12896  nnmaxpwlemnfac  12970  pceq0  13124  pcmpt  13145  prmlem0  13243  gzsumfzval  13764  ply1termlem  15934  lgseisenlem1  16355  lgsquadlem3  16364  2sqlem8a  16407  2sqlem8  16408  pwle2  17194  stnot  17205  wexmiddifxylem  17211