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  4101  fidifsnen  7040  php5fin  7052  tridc  7069  fimax2gtrilemstep  7070  en2eqpr  7077  inflbti  7199  omp1eomlem  7269  difinfsnlem  7274  addnidpig  7531  nqnq0pi  7633  ltpopr  7790  cauappcvgprlemladdru  7851  caucvgprlemladdrl  7873  caucvgprprlemnkltj  7884  caucvgprprlemnkeqj  7885  caucvgprprlemaddq  7903  ltposr  7958  axpre-suploclemres  8096  axltirr  8221  reapirr  8732  apirr  8760  indstr2  9812  xrltnsym  9997  xrlttr  9999  xrltso  10000  xltadd1  10080  xposdif  10086  xleaddadd  10091  lbioog  10117  ubioog  10118  fzn  10246  xqltnle  10495  flqltnz  10515  iseqf1olemnab  10731  iseqf1olemqk  10737  exp3val  10771  fihashelne0d  11027  zfz1isolemiso  11069  swrdnd  11199  swrd0g  11200  xrmaxltsup  11777  binomlem  12002  dvdsle  12363  2tp1odd  12403  divalglemeuneg  12442  bits0e  12468  bezoutlemle  12537  rpexp  12683  oddpwdclemxy  12699  oddpwdclemndvds  12701  sqpweven  12705  2sqpwodd  12706  oddprm  12790  pythagtriplem11  12805  pythagtriplem13  12807  pcpremul  12824  pczndvds2  12849  pc2dvds  12861  pcmpt  12874  ctinfom  13007  aprirr  14255  ivthinc  15325  logbgcd1irraplemexp  15650  lgsval2lem  15697  lgsdir  15722  lgsne0  15725  gausslemma2dlem1f1o  15747  lgseisenlem1  15757  lgseisenlem2  15758  lgseisenlem4  15760  lgsquadlem1  15764  lgsquad2  15770  m1lgs  15772  2sqlem7  15808  neapmkvlem  16465