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  2330  neleqtrrd  2333  eqnbrtrd  4132  fidifsnen  7138  php5fin  7152  tridc  7170  fimax2gtrilemstep  7171  en2eqpr  7180  inflbti  7328  omp1eomlem  7398  difinfsnlem  7403  addnidpig  7667  nqnq0pi  7769  ltpopr  7926  cauappcvgprlemladdru  7987  caucvgprlemladdrl  8009  caucvgprprlemnkltj  8020  caucvgprprlemnkeqj  8021  caucvgprprlemaddq  8039  ltposr  8094  axpre-suploclemres  8232  axltirr  8356  reapirr  8869  apirr  8897  indstr2  9962  xrltnsym  10148  xrlttr  10150  xrltso  10151  xltadd1  10231  xposdif  10237  xleaddadd  10242  lbioog  10268  ubioog  10269  fzn  10399  xqltnle  10654  flqltnz  10674  iseqf1olemnab  10890  iseqf1olemqk  10896  exp3val  10930  fihashelne0d  11188  zfz1isolemiso  11239  swrdnd  11379  swrd0g  11380  xrmaxltsup  11971  binomlem  12197  dvdsle  12558  2tp1odd  12598  divalglemeuneg  12637  bits0e  12663  bezoutlemle  12732  rpexp  12878  oddpwdclemxy  12894  oddpwdclemndvds  12896  sqpweven  12900  2sqpwodd  12901  oddprm  12985  pythagtriplem11  13000  pythagtriplem13  13002  pcpremul  13019  pczndvds2  13044  pc2dvds  13056  pcmpt  13069  ballotfilem4  13188  ctinfom  13266  aprirr  14536  ivthinc  15637  logbgcd1irraplemexp  15962  lgsval2lem  16012  lgsdir  16037  lgsne0  16040  gausslemma2dlem1f1o  16062  lgseisenlem1  16072  lgseisenlem2  16073  lgseisenlem4  16075  lgsquadlem1  16079  lgsquad2  16085  m1lgs  16087  2sqlem7  16123  1loopgrvd0fi  16430  qdiff  16972  neapmkvlem  16992