Theorem mtbird 662

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 143	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtod 652	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-in1 603  ax-in2 604

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  eqneltrd  2235  neleqtrrd  2238  fidifsnen  6764  php5fin  6776  tridc  6793  fimax2gtrilemstep  6794  en2eqpr  6801  inflbti  6911  omp1eomlem  6979  difinfsnlem  6984  addnidpig  7144  nqnq0pi  7246  ltpopr  7403  cauappcvgprlemladdru  7464  caucvgprlemladdrl  7486  caucvgprprlemnkltj  7497  caucvgprprlemnkeqj  7498  caucvgprprlemaddq  7516  ltposr  7571  axpre-suploclemres  7709  axltirr  7831  reapirr  8339  apirr  8367  indstr2  9403  xrltnsym  9579  xrlttr  9581  xrltso  9582  xltadd1  9659  xposdif  9665  xleaddadd  9670  lbioog  9696  ubioog  9697  fzn  9822  flqltnz  10060  iseqf1olemnab  10261  iseqf1olemqk  10267  exp3val  10295  zfz1isolemiso  10582  xrmaxltsup  11027  binomlem  11252  dvdsle  11542  2tp1odd  11581  divalglemeuneg  11620  bezoutlemle  11696  rpexp  11831  oddpwdclemxy  11847  oddpwdclemndvds  11849  sqpweven  11853  2sqpwodd  11854  ctinfom  11941  ivthinc  12790