MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtbii 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  1999  limom  4827  omopthlem2  6866  fineqv  7291  dfac2  7975  nd3  8428  axunndlem1  8434  axregndlem1  8441  axregndlem2  8442  axregnd  8443  axacndlem5  8450  canthp1lem2  8492  alephgch  8517  inatsk  8617  addnidpi  8742  indpi  8748  archnq  8821  fsumsplit  12496  sumsplit  12515  geoisum1c  12620  gexdvds  15181  chtub  20957  avril1  21718  vcoprne  22019  ballotlemi1  24721  ballotlemii  24722  fprodm1  25251  distel  25382  fvnobday  25558  onsucsuccmpi  26105  nvelim  27853  ax9NEW7  29186
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