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

Theorem mtbii 300
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 223 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3mtoi 178 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  limom  6688  omopthlem2  7297  fineqv  7728  dfac2  8502  nd3  8955  axunndlem1  8961  axregndlem1  8968  axregndlem2  8969  axregnd  8970  axregndOLD  8971  axacndlem5  8978  canthp1lem2  9020  alephgch  9041  inatsk  9145  addnidpi  9268  indpi  9274  archnq  9347  fsumsplit  13644  sumsplit  13665  geoisum1c  13771  fprodm1  13853  m1dvdsndvds  14409  gexdvds  16803  chtub  23685  avril1  25373  vcoprne  25670  ballotlemi1  28705  ballotlemii  28706  distel  29476  fvnobday  29682  onsucsuccmpi  30136  nvelim  32444  0nodd  32870  2nodd  32872  bj-inftyexpidisj  35013
  Copyright terms: Public domain W3C validator