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

Theorem mtbir 632
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 631 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  fal  1297  ax-9  1470  nonconne  2268  nemtbir  2345  ru  2840  noel  3291  iun0  3792  0iun  3793  vprc  3977  iin0r  4010  nlim0  4230  snnex  4283  onsucelsucexmid  4359  0nelxp  4479  dm0  4663  iprc  4714  co02  4957  0fv  5352  frec0g  6176  nnsucuniel  6270  1nen2  6631  fidcenumlemrk  6717  djulclb  6801  0nnq  6984  0npr  7103  nqprdisj  7164  0ncn  7430  axpre-ltirr  7478  pnfnre  7590  mnfnre  7591  inelr  8122  xrltnr  9311  fzo0  9640  fzouzdisj  9652  inftonninf  9908  hashinfom  10247  3prm  11449  sqrt2irr  11480  nnexmid  11933  nndc  11934  bj-vprc  12060  exmidsbthrlem  12184
  Copyright terms: Public domain W3C validator