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  4129  fidifsnen  7127  php5fin  7141  tridc  7159  fimax2gtrilemstep  7160  en2eqpr  7169  inflbti  7317  omp1eomlem  7387  difinfsnlem  7392  addnidpig  7656  nqnq0pi  7758  ltpopr  7915  cauappcvgprlemladdru  7976  caucvgprlemladdrl  7998  caucvgprprlemnkltj  8009  caucvgprprlemnkeqj  8010  caucvgprprlemaddq  8028  ltposr  8083  axpre-suploclemres  8221  axltirr  8345  reapirr  8856  apirr  8884  indstr2  9947  xrltnsym  10132  xrlttr  10134  xrltso  10135  xltadd1  10215  xposdif  10221  xleaddadd  10226  lbioog  10252  ubioog  10253  fzn  10382  xqltnle  10634  flqltnz  10654  iseqf1olemnab  10870  iseqf1olemqk  10876  exp3val  10910  fihashelne0d  11168  zfz1isolemiso  11219  swrdnd  11359  swrd0g  11360  xrmaxltsup  11951  binomlem  12177  dvdsle  12538  2tp1odd  12578  divalglemeuneg  12617  bits0e  12643  bezoutlemle  12712  rpexp  12858  oddpwdclemxy  12874  oddpwdclemndvds  12876  sqpweven  12880  2sqpwodd  12881  oddprm  12965  pythagtriplem11  12980  pythagtriplem13  12982  pcpremul  12999  pczndvds2  13024  pc2dvds  13036  pcmpt  13049  ballotfilem4  13163  ctinfom  13200  aprirr  14455  ivthinc  15557  logbgcd1irraplemexp  15882  lgsval2lem  15932  lgsdir  15957  lgsne0  15960  gausslemma2dlem1f1o  15982  lgseisenlem1  15992  lgseisenlem2  15993  lgseisenlem4  15995  lgsquadlem1  15999  lgsquad2  16005  m1lgs  16007  2sqlem7  16043  1loopgrvd0fi  16350  qdiff  16882  neapmkvlem  16902