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 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  7819  omopthlem2  8607  fineqv  9208  nd3  10526  axunndlem1  10532  axregndlem1  10539  axregndlem2  10540  axregnd  10541  axacndlem5  10548  canthp1lem2  10590  alephgch  10611  inatsk  10715  addnidpi  10838  indpi  10844  archnq  10917  fsumsplit  15627  sumsplit  15654  geoisum1c  15766  fprodm1  15851  m1dvdsndvds  16671  gexdvds  19367  chtub  26563  nolt02o  27046  nogt01o  27047  wlkp1lem6  28629  avril1  29410  ballotlemi1  33105  ballotlemii  33106  distel  34381  onsucsuccmpi  34918  bj-inftyexpitaudisj  35679  bj-inftyexpidisj  35684  poimirlem28  36109  poimirlem32  36113  n0eldmqseq  37114  lcmineqlem23  40511  nvelim  45362  0nodd  46111  2nodd  46113
  Copyright terms: Public domain W3C validator