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

Theorem mtbir 672
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 132 . 2 (𝜓𝜑)
41, 3mtbi 671 1 ¬ 𝜑
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  nnexmid  851  nndc  852  fal  1371  ax-9  1542  nonconne  2372  nemtbir  2449  ru  2976  noel  3441  iun0  3961  0iun  3962  br0  4069  vprc  4153  iin0r  4190  nlim0  4415  snnex  4469  onsucelsucexmid  4550  0nelxp  4675  dm0  4862  iprc  4916  co02  5163  0fv  5573  frec0g  6426  nnsucuniel  6524  1nen2  6893  fidcenumlemrk  6987  djulclb  7088  ismkvnex  7188  pw1ne3  7264  sucpw1nel3  7267  3nsssucpw1  7270  0nnq  7398  0npr  7517  nqprdisj  7578  0ncn  7865  axpre-ltirr  7916  pnfnre  8034  mnfnre  8035  inelr  8576  xrltnr  9815  fzo0  10204  fzouzdisj  10216  inftonninf  10479  hashinfom  10799  3prm  12171  sqrt2irr  12205  ennnfonelem1  12469  bj-nndcALT  14996  bj-vprc  15134  pwle2  15235  exmidsbthrlem  15258
  Copyright terms: Public domain W3C validator