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  6700  omopthlem2  7306  fineqv  7736  dfac2  8512  nd3  8965  axunndlem1  8971  axregndlem1  8980  axregndlem2  8981  axregnd  8982  axregndOLD  8983  axacndlem5  8990  canthp1lem2  9032  alephgch  9053  inatsk  9157  addnidpi  9280  indpi  9286  archnq  9359  fsumsplit  13528  sumsplit  13549  geoisum1c  13655  m1dvdsndvds  14187  gexdvds  16419  chtub  23312  avril1  24944  vcoprne  25245  ballotlemi1  28192  ballotlemii  28193  fprodm1  28949  distel  29089  fvnobday  29295  onsucsuccmpi  29761  nvelim  31899  bj-inftyexpidisj  33902
  Copyright terms: Public domain W3C validator