Theorem mtbird 684

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 673	1 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  eqneltrd  2334  neleqtrrd  2337  eqnbrtrd  4148  fidifsnen  7172  php5fin  7186  tridc  7204  fimax2gtrilemstep  7205  en2eqpr  7214  inflbti  7364  omp1eomlem  7434  difinfsnlem  7439  addnidpig  7703  nqnq0pi  7805  ltpopr  7962  cauappcvgprlemladdru  8023  caucvgprlemladdrl  8045  caucvgprprlemnkltj  8056  caucvgprprlemnkeqj  8057  caucvgprprlemaddq  8075  ltposr  8130  axpre-suploclemres  8268  axltirr  8392  reapirr  8906  apirr  8934  indstr2  10011  xrltnsym  10197  xrlttr  10199  xrltso  10200  xltadd1  10280  xposdif  10286  xleaddadd  10291  lbioog  10317  ubioog  10318  fzn  10448  xqltnle  10704  flqltnz  10724  iseqf1olemnab  10940  iseqf1olemqk  10946  exp3val  10980  fihashelne0d  11238  hashf1lem1  11287  zfz1isolemiso  11293  swrdnd  11433  swrd0g  11434  xrmaxltsup  12026  binomlem  12252  dvdsle  12613  2tp1odd  12653  divalglemeuneg  12692  bits0e  12718  bezoutlemle  12787  rpexp  12933  oddpwdclemxy  12949  oddpwdclemndvds  12951  sqpweven  12955  2sqpwodd  12956  oddprm  13040  pythagtriplem11  13055  pythagtriplem13  13057  pcpremul  13074  pczndvds2  13099  pc2dvds  13111  pcmpt  13124  ballotfilem4  13243  ctinfom  13321  aprirr  14597  ivthinc  15746  logbgcd1irraplemexp  16076  birthdaylem3  16095  lgsval2lem  16141  lgsdir  16166  lgsne0  16169  gausslemma2dlem1f1o  16191  lgseisenlem1  16201  lgseisenlem2  16202  lgseisenlem4  16204  lgsquadlem1  16208  lgsquad2  16214  m1lgs  16216  2sqlem7  16252  1loopgrvd0fi  16559  qdiff  17110  neapmkvlem  17129