MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtbii Structured version   Visualization version   GIF version

Theorem mtbii 326
Description: An inference from a biconditional, similar to modus tollens. (Contributed by NM, 27-Nov-1995.)
Hypotheses
Ref Expression
mtbii.min ¬ 𝜓
mtbii.maj (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mtbii (𝜑 → ¬ 𝜒)

Proof of Theorem mtbii
StepHypRef Expression
1 mtbii.min . 2 ¬ 𝜓
2 mtbii.maj . . 3 (𝜑 → (𝜓𝜒))
32biimprd 248 . 2 (𝜑 → (𝜒𝜓))
41, 3mtoi 199 1 (𝜑 → ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 207
This theorem is referenced by:  limom  7904  omopthlem2  8699  fineqv  9300  nd3  10630  axunndlem1  10636  axregndlem1  10643  axregndlem2  10644  axregnd  10645  axacndlem5  10652  canthp1lem2  10694  alephgch  10715  inatsk  10819  addnidpi  10942  indpi  10948  archnq  11021  fsumsplit  15778  sumsplit  15805  geoisum1c  15917  fprodm1  16004  m1dvdsndvds  16837  gexdvds  19603  chtub  27257  nolt02o  27741  nogt01o  27742  wlkp1lem6  29697  avril1  30483  ballotlemi1  34506  ballotlemii  34507  distel  35805  onsucsuccmpi  36445  bj-inftyexpitaudisj  37207  bj-inftyexpidisj  37212  poimirlem28  37656  poimirlem32  37660  n0eldmqseq  38651  lcmineqlem23  42053  nvelim  47140  0nodd  48091  2nodd  48093
  Copyright terms: Public domain W3C validator