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

Proof of Theorem mtbir
StepHypRef Expression
1 mtbir.1 . 2
2 mtbir.2 . . 3
32bicomi 127 . 2
41, 3mtbi 605 1
 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