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

Theorem mtbii 318
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 240 . 2 (𝜑 → (𝜒𝜓))
41, 3mtoi 191 1 (𝜑 → ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198
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 199
This theorem is referenced by:  limom  7312  omopthlem2  7974  fineqv  8415  dfac2OLD  9239  nd3  9697  axunndlem1  9703  axregndlem1  9710  axregndlem2  9711  axregnd  9712  axacndlem5  9719  canthp1lem2  9761  alephgch  9782  inatsk  9886  addnidpi  10009  indpi  10015  archnq  10088  fsumsplit  14809  sumsplit  14835  geoisum1c  14946  fprodm1  15031  m1dvdsndvds  15833  gexdvds  18309  chtub  25286  wlkp1lem6  26923  avril1  27839  ballotlemi1  31073  ballotlemii  31074  distel  32213  nolt02o  32350  onsucsuccmpi  32942  bj-inftyexpidisj  33588  poimirlem28  33918  poimirlem32  33922  nvelim  41965  0nodd  42597  2nodd  42599
  Copyright terms: Public domain W3C validator