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

Theorem mtbiri 635
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 625 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 579  ax-in2 580
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  n0i  3289  axnul  3956  intexr  3978  intnexr  3979  iin0r  3996  exmid01  4023  ordtriexmidlem  4326  ordtriexmidlem2  4327  ordtri2or2exmidlem  4332  onsucelsucexmidlem  4335  sucprcreg  4355  preleq  4361  reg3exmidlemwe  4384  dcextest  4386  nn0eln0  4423  0nelelxp  4456  tfrlemisucaccv  6072  nnsucuniel  6238  nndceq  6242  nndcel  6243  2dom  6502  snnen2oprc  6556  snexxph  6638  djune  6748  updjudhcoinrg  6751  exmidfodomrlemrALT  6808  elni2  6852  ltsopi  6858  ltsonq  6936  renepnf  7514  renemnf  7515  lt0ne0d  7967  nnne0  8422  nn0ge2m1nn  8703  nn0nepnf  8714  xrltnr  9219  pnfnlt  9226  nltmnf  9227  xrltnsym  9232  xrlttri3  9236  nltpnft  9248  ngtmnft  9249  xrrebnd  9250  fzpreddisj  9452  fzm1  9481  exfzdc  9616  m1exp1  10994  3prm  11203  bj-intexr  11456  bj-intnexr  11457  nninfalllemn  11555  nninfsellemeq  11563  exmidsbthrlem  11569
  Copyright terms: Public domain W3C validator