Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  mtbird GIF version

Theorem mtbird 663
 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
StepHypRef Expression
1 mtbird.min . 2 (𝜑 → ¬ 𝜒)
2 mtbird.maj . . 3 (𝜑 → (𝜓𝜒))
32biimpd 143 . 2 (𝜑 → (𝜓𝜒))
41, 3mtod 653 1 (𝜑 → ¬ 𝜓)
 Colors of variables: wff set class 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 604  ax-in2 605 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  eqneltrd  2253  neleqtrrd  2256  fidifsnen  6808  php5fin  6820  tridc  6837  fimax2gtrilemstep  6838  en2eqpr  6845  inflbti  6960  omp1eomlem  7028  difinfsnlem  7033  addnidpig  7239  nqnq0pi  7341  ltpopr  7498  cauappcvgprlemladdru  7559  caucvgprlemladdrl  7581  caucvgprprlemnkltj  7592  caucvgprprlemnkeqj  7593  caucvgprprlemaddq  7611  ltposr  7666  axpre-suploclemres  7804  axltirr  7927  reapirr  8435  apirr  8463  indstr2  9502  xrltnsym  9682  xrlttr  9684  xrltso  9685  xltadd1  9762  xposdif  9768  xleaddadd  9773  lbioog  9799  ubioog  9800  fzn  9926  flqltnz  10168  iseqf1olemnab  10369  iseqf1olemqk  10375  exp3val  10403  zfz1isolemiso  10692  xrmaxltsup  11137  binomlem  11362  dvdsle  11717  2tp1odd  11756  divalglemeuneg  11795  bezoutlemle  11872  rpexp  12007  oddpwdclemxy  12023  oddpwdclemndvds  12025  sqpweven  12029  2sqpwodd  12030  ctinfom  12129  ivthinc  12981  logbgcd1irraplemexp  13245  neapmkvlem  13600
 Copyright terms: Public domain W3C validator