Theorem mtbird 673

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 663	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 614  ax-in2 615

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eqneltrd  2273  neleqtrrd  2276  eqnbrtrd  4023  fidifsnen  6872  php5fin  6884  tridc  6901  fimax2gtrilemstep  6902  en2eqpr  6909  inflbti  7025  omp1eomlem  7095  difinfsnlem  7100  addnidpig  7337  nqnq0pi  7439  ltpopr  7596  cauappcvgprlemladdru  7657  caucvgprlemladdrl  7679  caucvgprprlemnkltj  7690  caucvgprprlemnkeqj  7691  caucvgprprlemaddq  7709  ltposr  7764  axpre-suploclemres  7902  axltirr  8026  reapirr  8536  apirr  8564  indstr2  9611  xrltnsym  9795  xrlttr  9797  xrltso  9798  xltadd1  9878  xposdif  9884  xleaddadd  9889  lbioog  9915  ubioog  9916  fzn  10044  flqltnz  10289  iseqf1olemnab  10490  iseqf1olemqk  10496  exp3val  10524  fihashelne0d  10779  zfz1isolemiso  10821  xrmaxltsup  11268  binomlem  11493  dvdsle  11852  2tp1odd  11891  divalglemeuneg  11930  bezoutlemle  12011  rpexp  12155  oddpwdclemxy  12171  oddpwdclemndvds  12173  sqpweven  12177  2sqpwodd  12178  oddprm  12261  pythagtriplem11  12276  pythagtriplem13  12278  pcpremul  12295  pczndvds2  12319  pc2dvds  12331  pcmpt  12343  ctinfom  12431  aprirr  13378  ivthinc  14160  logbgcd1irraplemexp  14425  lgsval2lem  14450  lgsdir  14475  lgsne0  14478  lgseisenlem1  14489  lgseisenlem2  14490  m1lgs  14491  2sqlem7  14507  neapmkvlem  14853