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

Theorem mtbir 629
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 130 . 2 (𝜓𝜑)
41, 3mtbi 628 1 ¬ 𝜑
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  fal  1292  ax-9  1465  nonconne  2261  nemtbir  2338  ru  2825  noel  3273  iun0  3760  0iun  3761  vprc  3936  iin0r  3969  nlim0  4185  snnex  4235  onsucelsucexmid  4309  0nelxp  4428  dm0  4608  iprc  4659  co02  4898  0fv  5284  frec0g  6094  nnsucuniel  6188  1nen2  6507  djulclb  6654  0nnq  6826  0npr  6945  nqprdisj  7006  0ncn  7272  axpre-ltirr  7320  pnfnre  7432  mnfnre  7433  inelr  7961  xrltnr  9145  fzo0  9468  fzouzdisj  9480  inftonninf  9736  hashinfom  10021  3prm  10890  sqrt2irr  10921  nnexmid  11003  nndc  11004  bj-vprc  11130  exmidsbthrlem  11254
  Copyright terms: Public domain W3C validator