Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  mtbir GIF 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 ¬ 𝜓
mtbir.2 (𝜑𝜓)
Assertion
Ref Expression
mtbir ¬ 𝜑

Proof of Theorem mtbir
StepHypRef Expression
1 mtbir.1 . 2 ¬ 𝜓
2 mtbir.2 . . 3 (𝜑𝜓)
32bicomi 131 . 2 (𝜓𝜑)
41, 3mtbi 659 1 ¬ 𝜑
 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  3872  0iun  3873  br0  3979  vprc  4063  iin0r  4096  nlim0  4319  snnex  4372  onsucelsucexmid  4448  0nelxp  4570  dm0  4756  iprc  4810  co02  5055  0fv  5459  frec0g  6297  nnsucuniel  6394  1nen2  6758  fidcenumlemrk  6845  djulclb  6943  ismkvnex  7032  0nnq  7191  0npr  7310  nqprdisj  7371  0ncn  7658  axpre-ltirr  7709  pnfnre  7826  mnfnre  7827  inelr  8365  xrltnr  9589  fzo0  9969  fzouzdisj  9981  inftonninf  10238  hashinfom  10548  3prm  11832  sqrt2irr  11863  ennnfonelem1  11943  bj-nndcALT  13107  bj-vprc  13238  pwle2  13339  exmidsbthrlem  13365
 Copyright terms: Public domain W3C validator