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  1889  limom  4671  omopthlem2  6654  fineqv  7078  dfac2  7757  nd3  8211  axunndlem1  8217  axregndlem1  8224  axregndlem2  8225  axregnd  8226  axacndlem5  8233  canthp1lem2  8275  alephgch  8300  inatsk  8400  addnidpi  8525  indpi  8531  archnq  8604  fsumsplit  12212  sumsplit  12231  geoisum1c  12336  gexdvds  14895  chtub  20451  avril1  20836  vcoprne  21135  distel  24160  fvnobday  24336  onsucsuccmpi  24882  nvelim  27978  afvvfveq  28011  ax12-2  29103
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