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

Theorem mtbii 293
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 214 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3mtoi 169 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  ax9  1954  limom  4753  omopthlem2  6741  fineqv  7166  dfac2  7847  nd3  8301  axunndlem1  8307  axregndlem1  8314  axregndlem2  8315  axregnd  8316  axacndlem5  8323  canthp1lem2  8365  alephgch  8390  inatsk  8490  addnidpi  8615  indpi  8621  archnq  8694  fsumsplit  12309  sumsplit  12328  geoisum1c  12433  gexdvds  14994  chtub  20563  avril1  20948  vcoprne  21249  fprodm1  24591  distel  24718  fvnobday  24894  onsucsuccmpi  25441  nvelim  27301  afvvfveq  27336  ax9NEW7  28891  ax12-2  29172
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 177
  Copyright terms: Public domain W3C validator