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

Theorem mtbii 294
Description: An inference from a biconditional, similar to modus tollens. (Contributed by NM, 27-Nov-1995.)
Hypotheses
Ref Expression
mtbii.min  |-  -.  ps
mtbii.maj  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
mtbii  |-  ( ph  ->  -.  ch )

Proof of Theorem mtbii
StepHypRef Expression
1 mtbii.min . 2  |-  -.  ps
2 mtbii.maj . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
32biimprd 215 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3mtoi 171 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177
This theorem is referenced by:  ax9OLD  2033  limom  4860  omopthlem2  6899  fineqv  7324  dfac2  8011  nd3  8464  axunndlem1  8470  axregndlem1  8477  axregndlem2  8478  axregnd  8479  axacndlem5  8486  canthp1lem2  8528  alephgch  8553  inatsk  8653  addnidpi  8778  indpi  8784  archnq  8857  fsumsplit  12533  sumsplit  12552  geoisum1c  12657  gexdvds  15218  chtub  20996  avril1  21757  vcoprne  22058  ballotlemi1  24760  ballotlemii  24761  fprodm1  25290  distel  25431  fvnobday  25637  onsucsuccmpi  26193  nvelim  27954  ax9NEW7  29468
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator