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

Theorem mtbiri 647
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 143 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtoi 636 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-in1 586  ax-in2 587
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  n0i  3336  axnul  4021  intexr  4043  intnexr  4044  iin0r  4061  exmid01  4089  ordtriexmidlem  4403  ordtriexmidlem2  4404  ordtri2or2exmidlem  4409  onsucelsucexmidlem  4412  sucprcreg  4432  preleq  4438  reg3exmidlemwe  4461  dcextest  4463  nn0eln0  4501  0nelelxp  4536  tfrlemisucaccv  6188  nnsucuniel  6357  nndceq  6361  nndcel  6362  2dom  6665  snnen2oprc  6720  snexxph  6804  elfi2  6826  djune  6929  updjudhcoinrg  6932  omp1eomlem  6945  ismkvnex  6995  mkvprop  6998  exmidfodomrlemrALT  7023  exmidaclem  7028  elni2  7086  ltsopi  7092  ltsonq  7170  renepnf  7777  renemnf  7778  lt0ne0d  8239  sup3exmid  8675  nnne0  8708  nn0ge2m1nn  8991  nn0nepnf  9002  xrltnr  9517  pnfnlt  9524  nltmnf  9525  xrltnsym  9530  xrlttri3  9534  nltpnft  9548  ngtmnft  9551  xrrebnd  9553  xrpnfdc  9576  xrmnfdc  9577  xsubge0  9615  xposdif  9616  xleaddadd  9621  fzpreddisj  9802  fzm1  9831  exfzdc  9968  xrbdtri  10996  m1exp1  11505  3prm  11716  exmidunben  11845  unct  11860  blssioo  12620  bj-intexr  12940  bj-intnexr  12941  subctctexmid  13030  nninfalllemn  13036  nninfsellemeq  13044  exmidsbthrlem  13051
  Copyright terms: Public domain W3C validator