Theorem mtbird 684

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 673	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 623  ax-in2 624

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eqneltrd  2334  neleqtrrd  2337  eqnbrtrd  4146  fidifsnen  7166  php5fin  7180  tridc  7198  fimax2gtrilemstep  7199  en2eqpr  7208  inflbti  7358  omp1eomlem  7428  difinfsnlem  7433  addnidpig  7697  nqnq0pi  7799  ltpopr  7956  cauappcvgprlemladdru  8017  caucvgprlemladdrl  8039  caucvgprprlemnkltj  8050  caucvgprprlemnkeqj  8051  caucvgprprlemaddq  8069  ltposr  8124  axpre-suploclemres  8262  axltirr  8386  reapirr  8899  apirr  8927  indstr2  9992  xrltnsym  10178  xrlttr  10180  xrltso  10181  xltadd1  10261  xposdif  10267  xleaddadd  10272  lbioog  10298  ubioog  10299  fzn  10429  xqltnle  10685  flqltnz  10705  iseqf1olemnab  10921  iseqf1olemqk  10927  exp3val  10961  fihashelne0d  11219  hashf1lem1  11268  zfz1isolemiso  11274  swrdnd  11414  swrd0g  11415  xrmaxltsup  12007  binomlem  12233  dvdsle  12594  2tp1odd  12634  divalglemeuneg  12673  bits0e  12699  bezoutlemle  12768  rpexp  12914  oddpwdclemxy  12930  oddpwdclemndvds  12932  sqpweven  12936  2sqpwodd  12937  oddprm  13021  pythagtriplem11  13036  pythagtriplem13  13038  pcpremul  13055  pczndvds2  13080  pc2dvds  13092  pcmpt  13105  ballotfilem4  13224  ctinfom  13302  aprirr  14578  ivthinc  15727  logbgcd1irraplemexp  16053  birthdaylem3  16072  lgsval2lem  16112  lgsdir  16137  lgsne0  16140  gausslemma2dlem1f1o  16162  lgseisenlem1  16172  lgseisenlem2  16173  lgseisenlem4  16175  lgsquadlem1  16179  lgsquad2  16185  m1lgs  16187  2sqlem7  16223  1loopgrvd0fi  16530  qdiff  17072  neapmkvlem  17091