Theorem mtbird 679

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  2326  neleqtrrd  2329  eqnbrtrd  4107  fidifsnen  7062  php5fin  7076  tridc  7094  fimax2gtrilemstep  7095  en2eqpr  7104  inflbti  7228  omp1eomlem  7298  difinfsnlem  7303  addnidpig  7561  nqnq0pi  7663  ltpopr  7820  cauappcvgprlemladdru  7881  caucvgprlemladdrl  7903  caucvgprprlemnkltj  7914  caucvgprprlemnkeqj  7915  caucvgprprlemaddq  7933  ltposr  7988  axpre-suploclemres  8126  axltirr  8251  reapirr  8762  apirr  8790  indstr2  9848  xrltnsym  10033  xrlttr  10035  xrltso  10036  xltadd1  10116  xposdif  10122  xleaddadd  10127  lbioog  10153  ubioog  10154  fzn  10282  xqltnle  10533  flqltnz  10553  iseqf1olemnab  10769  iseqf1olemqk  10775  exp3val  10809  fihashelne0d  11065  zfz1isolemiso  11109  swrdnd  11249  swrd0g  11250  xrmaxltsup  11841  binomlem  12067  dvdsle  12428  2tp1odd  12468  divalglemeuneg  12507  bits0e  12533  bezoutlemle  12602  rpexp  12748  oddpwdclemxy  12764  oddpwdclemndvds  12766  sqpweven  12770  2sqpwodd  12771  oddprm  12855  pythagtriplem11  12870  pythagtriplem13  12872  pcpremul  12889  pczndvds2  12914  pc2dvds  12926  pcmpt  12939  ctinfom  13072  aprirr  14321  ivthinc  15396  logbgcd1irraplemexp  15721  lgsval2lem  15768  lgsdir  15793  lgsne0  15796  gausslemma2dlem1f1o  15818  lgseisenlem1  15828  lgseisenlem2  15829  lgseisenlem4  15831  lgsquadlem1  15835  lgsquad2  15841  m1lgs  15843  2sqlem7  15879  1loopgrvd0fi  16186  qdiff  16720  neapmkvlem  16739