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 237 . 2 (𝜑 → (𝜒𝜓))
41, 3mtoi 189 1 (𝜑 → ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195
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 196
This theorem is referenced by:  limom  6950  omopthlem2  7601  fineqv  8038  dfac2  8814  nd3  9268  axunndlem1  9274  axregndlem1  9281  axregndlem2  9282  axregnd  9283  axacndlem5  9290  canthp1lem2  9332  alephgch  9353  inatsk  9457  addnidpi  9580  indpi  9586  archnq  9659  fsumsplit  14267  sumsplit  14290  geoisum1c  14399  fprodm1  14485  m1dvdsndvds  15290  gexdvds  17771  chtub  24682  avril1  26505  ballotlemi1  29685  ballotlemii  29686  distel  30747  fvnobday  30875  onsucsuccmpi  31406  bj-inftyexpidisj  32068  poimirlem28  32401  poimirlem32  32405  nvelim  39643  1wlkp1lem6  40879  0nodd  41592  2nodd  41594
  Copyright terms: Public domain W3C validator