Theorem mtbird 677

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 667	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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eqneltrd  2325  neleqtrrd  2328  eqnbrtrd  4104  fidifsnen  7052  php5fin  7066  tridc  7084  fimax2gtrilemstep  7085  en2eqpr  7094  inflbti  7217  omp1eomlem  7287  difinfsnlem  7292  addnidpig  7549  nqnq0pi  7651  ltpopr  7808  cauappcvgprlemladdru  7869  caucvgprlemladdrl  7891  caucvgprprlemnkltj  7902  caucvgprprlemnkeqj  7903  caucvgprprlemaddq  7921  ltposr  7976  axpre-suploclemres  8114  axltirr  8239  reapirr  8750  apirr  8778  indstr2  9836  xrltnsym  10021  xrlttr  10023  xrltso  10024  xltadd1  10104  xposdif  10110  xleaddadd  10115  lbioog  10141  ubioog  10142  fzn  10270  xqltnle  10520  flqltnz  10540  iseqf1olemnab  10756  iseqf1olemqk  10762  exp3val  10796  fihashelne0d  11052  zfz1isolemiso  11096  swrdnd  11233  swrd0g  11234  xrmaxltsup  11812  binomlem  12037  dvdsle  12398  2tp1odd  12438  divalglemeuneg  12477  bits0e  12503  bezoutlemle  12572  rpexp  12718  oddpwdclemxy  12734  oddpwdclemndvds  12736  sqpweven  12740  2sqpwodd  12741  oddprm  12825  pythagtriplem11  12840  pythagtriplem13  12842  pcpremul  12859  pczndvds2  12884  pc2dvds  12896  pcmpt  12909  ctinfom  13042  aprirr  14290  ivthinc  15360  logbgcd1irraplemexp  15685  lgsval2lem  15732  lgsdir  15757  lgsne0  15760  gausslemma2dlem1f1o  15782  lgseisenlem1  15792  lgseisenlem2  15793  lgseisenlem4  15795  lgsquadlem1  15799  lgsquad2  15805  m1lgs  15807  2sqlem7  15843  1loopgrvd0fi  16117  neapmkvlem  16621