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

Theorem mtbir 660
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 131 . 2  |-  ( ps  <->  ph )
41, 3mtbi 659 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  nnexmid  835  nndc  836  fal  1338  ax-9  1511  nonconne  2320  nemtbir  2397  ru  2908  noel  3367  iun0  3869  0iun  3870  br0  3976  vprc  4060  iin0r  4093  nlim0  4316  snnex  4369  onsucelsucexmid  4445  0nelxp  4567  dm0  4753  iprc  4807  co02  5052  0fv  5456  frec0g  6294  nnsucuniel  6391  1nen2  6755  fidcenumlemrk  6842  djulclb  6940  ismkvnex  7029  0nnq  7184  0npr  7303  nqprdisj  7364  0ncn  7651  axpre-ltirr  7702  pnfnre  7819  mnfnre  7820  inelr  8358  xrltnr  9578  fzo0  9957  fzouzdisj  9969  inftonninf  10226  hashinfom  10536  3prm  11820  sqrt2irr  11851  ennnfonelem1  11931  bj-nndcALT  13022  bj-vprc  13153  pwle2  13252  exmidsbthrlem  13278
  Copyright terms: Public domain W3C validator