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

Theorem mtbir 595
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
mtbir.2
Assertion
Ref Expression
mtbir

Proof of Theorem mtbir
StepHypRef Expression
1 mtbir.1 . 2
2 mtbir.2 . . 3
32bicomi 123 . 2
41, 3mtbi 594 1
Colors of variables: wff set class
Syntax hints:   wn 3   wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  fal  1249  ax-9  1421  nonconne  2212  nemtbir  2288  ru  2757  pssirr  3038  noel  3222  npss0  3260  iun0  3704  0iun  3705  vprc  3879  iin0r  3913  nlim0  4097  snnex  4147  onsucelsucexmid  4215  0nelxp  4315  dm0  4492  iprc  4543  co02  4777  0fv  5151  frec0g  5922  0nnq  6348  0npr  6466  nqprdisj  6527  0ncn  6729  axpre-ltirr  6766  pnfnre  6864  mnfnre  6865  inelr  7368  xrltnr  8471  fzo0  8794  fzouzdisj  8806  nnexmid  9234  nndc  9235  bj-vprc  9351
  Copyright terms: Public domain W3C validator