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

Theorem mtbii 325
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 247 . 2 (𝜑 → (𝜒𝜓))
41, 3mtoi 198 1 (𝜑 → ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205
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 206
This theorem is referenced by:  limom  7884  omopthlem2  8682  fineqv  9290  nd3  10623  axunndlem1  10629  axregndlem1  10636  axregndlem2  10637  axregnd  10638  axacndlem5  10645  canthp1lem2  10687  alephgch  10708  inatsk  10812  addnidpi  10935  indpi  10941  archnq  11014  fsumsplit  15740  sumsplit  15767  geoisum1c  15879  fprodm1  15964  m1dvdsndvds  16795  gexdvds  19578  chtub  27238  nolt02o  27722  nogt01o  27723  wlkp1lem6  29612  avril1  30393  ballotlemi1  34349  ballotlemii  34350  distel  35640  onsucsuccmpi  36168  bj-inftyexpitaudisj  36925  bj-inftyexpidisj  36930  poimirlem28  37362  poimirlem32  37366  n0eldmqseq  38360  lcmineqlem23  41763  nvelim  46772  0nodd  47583  2nodd  47585
  Copyright terms: Public domain W3C validator