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

Theorem mtbir 634
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 633 1 ¬ 𝜑
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 582  ax-in2 583
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  fal  1303  ax-9  1476  nonconne  2274  nemtbir  2351  ru  2853  noel  3306  iun0  3808  0iun  3809  vprc  3992  iin0r  4025  nlim0  4245  snnex  4298  onsucelsucexmid  4374  0nelxp  4495  dm0  4681  iprc  4733  co02  4978  0fv  5374  frec0g  6200  nnsucuniel  6296  1nen2  6657  fidcenumlemrk  6743  djulclb  6827  0nnq  7020  0npr  7139  nqprdisj  7200  0ncn  7466  axpre-ltirr  7514  pnfnre  7626  mnfnre  7627  inelr  8158  xrltnr  9349  fzo0  9728  fzouzdisj  9740  inftonninf  9996  hashinfom  10317  3prm  11552  sqrt2irr  11583  nnexmid  12372  nndc  12373  bj-vprc  12499  exmidsbthrlem  12621
  Copyright terms: Public domain W3C validator