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

Theorem mtbii 303
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 226 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3mtoi 181 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  limom  6665  omopthlem2  7312  fineqv  7740  dfac2  8512  nd3  8965  axunndlem1  8971  axregndlem1  8978  axregndlem2  8979  axregnd  8980  axacndlem5  8987  canthp1lem2  9029  alephgch  9050  inatsk  9154  addnidpi  9277  indpi  9283  archnq  9356  fsumsplit  13749  sumsplit  13772  geoisum1c  13879  fprodm1  13964  m1dvdsndvds  14692  gexdvds  17178  chtub  24082  avril1  25842  vcoprne  26140  ballotlemi1  29287  ballotlemii  29288  ballotlemi1OLD  29325  ballotlemiiOLD  29326  distel  30401  fvnobday  30520  onsucsuccmpi  31052  bj-inftyexpidisj  31559  poimirlem28  31875  poimirlem32  31879  nvelim  38435  0nodd  39401  2nodd  39403
  Copyright terms: Public domain W3C validator