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  7822  omopthlem2  8585  fineqv  9168  nelaneq  9512  nd3  10502  axunndlem1  10508  axregndlem1  10515  axregndlem2  10516  axregnd  10517  axacndlem5  10524  canthp1lem2  10566  alephgch  10587  inatsk  10691  addnidpi  10814  indpi  10820  archnq  10893  fsumsplit  15666  sumsplit  15693  geoisum1c  15805  fprodm1  15892  m1dvdsndvds  16728  gexdvds  19481  chtub  27139  nolt02o  27623  nogt01o  27624  wlkp1lem6  29640  avril1  30425  ballotlemi1  34473  ballotlemii  34474  onvf1odlem1  35078  distel  35779  onsucsuccmpi  36419  bj-inftyexpitaudisj  37181  bj-inftyexpidisj  37186  poimirlem28  37630  poimirlem32  37634  n0eldmqseq  38629  lcmineqlem23  42027  nvelim  47111  0nodd  48158  2nodd  48160
  Copyright terms: Public domain W3C validator