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

Theorem mtbii 329
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 251 . 2 (𝜑 → (𝜒𝜓))
41, 3mtoi 202 1 (𝜑 → ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209
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 210
This theorem is referenced by:  limom  7578  omopthlem2  8266  fineqv  8717  nd3  9996  axunndlem1  10002  axregndlem1  10009  axregndlem2  10010  axregnd  10011  axacndlem5  10018  canthp1lem2  10060  alephgch  10081  inatsk  10185  addnidpi  10308  indpi  10314  archnq  10387  fsumsplit  15086  sumsplit  15112  geoisum1c  15225  fprodm1  15310  m1dvdsndvds  16122  gexdvds  18698  chtub  25785  wlkp1lem6  27457  avril1  28237  ballotlemi1  31778  ballotlemii  31779  distel  33066  nolt02o  33217  onsucsuccmpi  33809  bj-inftyexpitaudisj  34523  bj-inftyexpidisj  34528  poimirlem28  34985  poimirlem32  34989  n0eldmqseq  35944  lcmineqlem23  39235  nvelim  43521  0nodd  44272  2nodd  44274
  Copyright terms: Public domain W3C validator