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  4021  fidifsnen  6869  php5fin  6881  tridc  6898  fimax2gtrilemstep  6899  en2eqpr  6906  inflbti  7022  omp1eomlem  7092  difinfsnlem  7097  addnidpig  7334  nqnq0pi  7436  ltpopr  7593  cauappcvgprlemladdru  7654  caucvgprlemladdrl  7676  caucvgprprlemnkltj  7687  caucvgprprlemnkeqj  7688  caucvgprprlemaddq  7706  ltposr  7761  axpre-suploclemres  7899  axltirr  8023  reapirr  8533  apirr  8561  indstr2  9608  xrltnsym  9792  xrlttr  9794  xrltso  9795  xltadd1  9875  xposdif  9881  xleaddadd  9886  lbioog  9912  ubioog  9913  fzn  10041  flqltnz  10286  iseqf1olemnab  10487  iseqf1olemqk  10493  exp3val  10521  fihashelne0d  10776  zfz1isolemiso  10818  xrmaxltsup  11265  binomlem  11490  dvdsle  11849  2tp1odd  11888  divalglemeuneg  11927  bezoutlemle  12008  rpexp  12152  oddpwdclemxy  12168  oddpwdclemndvds  12170  sqpweven  12174  2sqpwodd  12175  oddprm  12258  pythagtriplem11  12273  pythagtriplem13  12275  pcpremul  12292  pczndvds2  12316  pc2dvds  12328  pcmpt  12340  ctinfom  12428  aprirr  13371  ivthinc  14091  logbgcd1irraplemexp  14356  lgsval2lem  14381  lgsdir  14406  lgsne0  14409  lgseisenlem1  14420  lgseisenlem2  14421  m1lgs  14422  2sqlem7  14438  neapmkvlem  14784