ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mtbiri Unicode version

Theorem mtbiri 633
Description: An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.)
Hypotheses
Ref Expression
mtbiri.min  |-  -.  ch
mtbiri.maj  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
mtbiri  |-  ( ph  ->  -.  ps )

Proof of Theorem mtbiri
StepHypRef Expression
1 mtbiri.min . 2  |-  -.  ch
2 mtbiri.maj . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
32biimpd 142 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtoi 623 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-in1 577  ax-in2 578
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  n0i  3263  axnul  3911  intexr  3933  intnexr  3934  iin0r  3951  ordtriexmidlem  4271  ordtriexmidlem2  4272  ordtri2or2exmidlem  4277  onsucelsucexmidlem  4280  sucprcreg  4300  preleq  4306  reg3exmidlemwe  4329  nn0eln0  4367  0nelelxp  4399  tfrlemisucaccv  5974  nnsucuniel  6139  nndceq  6143  nndcel  6144  2dom  6352  snnen2oprc  6395  elni2  6566  ltsopi  6572  ltsonq  6650  renepnf  7228  renemnf  7229  lt0ne0d  7681  nnne0  8134  nn0ge2m1nn  8415  nn0nepnf  8426  xrltnr  8931  pnfnlt  8938  nltmnf  8939  xrltnsym  8944  xrlttri3  8948  nltpnft  8960  ngtmnft  8961  xrrebnd  8962  fzpreddisj  9164  fzm1  9193  exfzdc  9326  m1exp1  10445  3prm  10654  bj-intexr  10857  bj-intnexr  10858
  Copyright terms: Public domain W3C validator