Theorem mtbird 668

Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 10-May-1994.)

Hypotheses

Ref	Expression
mtbird.min	⊢ (𝜑 → ¬ 𝜒)
mtbird.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mtbird	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem mtbird

Step	Hyp	Ref	Expression
1		mtbird.min	. 2 ⊢ (𝜑 → ¬ 𝜒)
2		mtbird.maj	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	biimpd 143	. 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-in1 609  ax-in2 610

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  eqneltrd  2266  neleqtrrd  2269  eqnbrtrd  4007  fidifsnen  6848  php5fin  6860  tridc  6877  fimax2gtrilemstep  6878  en2eqpr  6885  inflbti  7001  omp1eomlem  7071  difinfsnlem  7076  addnidpig  7298  nqnq0pi  7400  ltpopr  7557  cauappcvgprlemladdru  7618  caucvgprlemladdrl  7640  caucvgprprlemnkltj  7651  caucvgprprlemnkeqj  7652  caucvgprprlemaddq  7670  ltposr  7725  axpre-suploclemres  7863  axltirr  7986  reapirr  8496  apirr  8524  indstr2  9568  xrltnsym  9750  xrlttr  9752  xrltso  9753  xltadd1  9833  xposdif  9839  xleaddadd  9844  lbioog  9870  ubioog  9871  fzn  9998  flqltnz  10243  iseqf1olemnab  10444  iseqf1olemqk  10450  exp3val  10478  fihashelne0d  10732  zfz1isolemiso  10774  xrmaxltsup  11221  binomlem  11446  dvdsle  11804  2tp1odd  11843  divalglemeuneg  11882  bezoutlemle  11963  rpexp  12107  oddpwdclemxy  12123  oddpwdclemndvds  12125  sqpweven  12129  2sqpwodd  12130  oddprm  12213  pythagtriplem11  12228  pythagtriplem13  12230  pcpremul  12247  pczndvds2  12271  pc2dvds  12283  pcmpt  12295  ctinfom  12383  ivthinc  13415  logbgcd1irraplemexp  13680  lgsval2lem  13705  lgsdir  13730  lgsne0  13733  2sqlem7  13751  neapmkvlem  14098