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

Theorem mtbir 606
Description: An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 14-Oct-2012.)
Hypotheses
Ref Expression
mtbir.1  |-  -.  ps
mtbir.2  |-  ( ph  <->  ps )
Assertion
Ref Expression
mtbir  |-  -.  ph

Proof of Theorem mtbir
StepHypRef Expression
1 mtbir.1 . 2  |-  -.  ps
2 mtbir.2 . . 3  |-  ( ph  <->  ps )
32bicomi 127 . 2  |-  ( ps  <->  ph )
41, 3mtbi 605 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  fal  1266  ax-9  1440  nonconne  2232  nemtbir  2309  ru  2786  pssirr  3072  noel  3256  npss0  3294  iun0  3741  0iun  3742  vprc  3916  iin0r  3950  nlim0  4159  snnex  4209  onsucelsucexmid  4283  0nelxp  4400  dm0  4577  iprc  4628  co02  4862  0fv  5236  frec0g  6014  0nnq  6520  0npr  6639  nqprdisj  6700  0ncn  6966  axpre-ltirr  7014  pnfnre  7126  mnfnre  7127  inelr  7649  xrltnr  8802  fzo0  9126  fzouzdisj  9138  sqrt2irr  10251  nnexmid  10286  nndc  10287  bj-vprc  10403
  Copyright terms: Public domain W3C validator