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  8022  reapirr  8532  apirr  8560  indstr2  9607  xrltnsym  9791  xrlttr  9793  xrltso  9794  xltadd1  9874  xposdif  9880  xleaddadd  9885  lbioog  9911  ubioog  9912  fzn  10039  flqltnz  10284  iseqf1olemnab  10485  iseqf1olemqk  10491  exp3val  10519  fihashelne0d  10772  zfz1isolemiso  10814  xrmaxltsup  11261  binomlem  11486  dvdsle  11844  2tp1odd  11883  divalglemeuneg  11922  bezoutlemle  12003  rpexp  12147  oddpwdclemxy  12163  oddpwdclemndvds  12165  sqpweven  12169  2sqpwodd  12170  oddprm  12253  pythagtriplem11  12268  pythagtriplem13  12270  pcpremul  12287  pczndvds2  12311  pc2dvds  12323  pcmpt  12335  ctinfom  12423  aprirr  13294  ivthinc  14014  logbgcd1irraplemexp  14279  lgsval2lem  14304  lgsdir  14329  lgsne0  14332  2sqlem7  14350  neapmkvlem  14696