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

Theorem mtbii 315
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 238 . 2 (𝜑 → (𝜒𝜓))
41, 3mtoi 190 1 (𝜑 → ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196
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 197
This theorem is referenced by:  limom  7122  omopthlem2  7781  fineqv  8216  dfac2  8991  nd3  9449  axunndlem1  9455  axregndlem1  9462  axregndlem2  9463  axregnd  9464  axacndlem5  9471  canthp1lem2  9513  alephgch  9534  inatsk  9638  addnidpi  9761  indpi  9767  archnq  9840  fsumsplit  14515  sumsplit  14543  geoisum1c  14655  fprodm1  14741  m1dvdsndvds  15550  gexdvds  18045  chtub  24982  wlkp1lem6  26631  avril1  27449  ballotlemi1  30692  ballotlemii  30693  distel  31833  nolt02o  31970  onsucsuccmpi  32567  bj-inftyexpidisj  33227  poimirlem28  33567  poimirlem32  33571  nvelim  41521  0nodd  42135  2nodd  42137
  Copyright terms: Public domain W3C validator