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

Theorem mtbii 302
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  6491  omopthlem2  7095  fineqv  7528  dfac2  8300  nd3  8753  axunndlem1  8759  axregndlem1  8768  axregndlem2  8769  axregnd  8770  axregndOLD  8771  axacndlem5  8778  canthp1lem2  8820  alephgch  8841  inatsk  8945  addnidpi  9070  indpi  9076  archnq  9149  fsumsplit  13216  sumsplit  13235  geoisum1c  13340  gexdvds  16083  chtub  22551  avril1  23656  vcoprne  23957  ballotlemi1  26885  ballotlemii  26886  fprodm1  27477  distel  27617  fvnobday  27823  onsucsuccmpi  28289  nvelim  30024  m1dvdsndvds  30247  bj-inftyexpidisj  32533
  Copyright terms: Public domain W3C validator