Theorem mtbird 680

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 144	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtod 669	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-in1 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eqneltrd  2328  neleqtrrd  2331  eqnbrtrd  4126  fidifsnen  7124  php5fin  7138  tridc  7156  fimax2gtrilemstep  7157  en2eqpr  7166  inflbti  7314  omp1eomlem  7384  difinfsnlem  7389  addnidpig  7647  nqnq0pi  7749  ltpopr  7906  cauappcvgprlemladdru  7967  caucvgprlemladdrl  7989  caucvgprprlemnkltj  8000  caucvgprprlemnkeqj  8001  caucvgprprlemaddq  8019  ltposr  8074  axpre-suploclemres  8212  axltirr  8336  reapirr  8847  apirr  8875  indstr2  9937  xrltnsym  10122  xrlttr  10124  xrltso  10125  xltadd1  10205  xposdif  10211  xleaddadd  10216  lbioog  10242  ubioog  10243  fzn  10372  xqltnle  10623  flqltnz  10643  iseqf1olemnab  10859  iseqf1olemqk  10865  exp3val  10899  fihashelne0d  11155  zfz1isolemiso  11204  swrdnd  11344  swrd0g  11345  xrmaxltsup  11936  binomlem  12162  dvdsle  12523  2tp1odd  12563  divalglemeuneg  12602  bits0e  12628  bezoutlemle  12697  rpexp  12843  oddpwdclemxy  12859  oddpwdclemndvds  12861  sqpweven  12865  2sqpwodd  12866  oddprm  12950  pythagtriplem11  12965  pythagtriplem13  12967  pcpremul  12984  pczndvds2  13009  pc2dvds  13021  pcmpt  13034  ctinfom  13168  aprirr  14418  ivthinc  15495  logbgcd1irraplemexp  15820  lgsval2lem  15870  lgsdir  15895  lgsne0  15898  gausslemma2dlem1f1o  15920  lgseisenlem1  15930  lgseisenlem2  15931  lgseisenlem4  15933  lgsquadlem1  15937  lgsquad2  15943  m1lgs  15945  2sqlem7  15981  1loopgrvd0fi  16288  qdiff  16820  neapmkvlem  16839