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

Theorem mtbir 645
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 644 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 588  ax-in2 589
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  nnexmid  820  nndc  821  fal  1323  ax-9  1496  nonconne  2297  nemtbir  2374  ru  2881  noel  3337  iun0  3839  0iun  3840  br0  3946  vprc  4030  iin0r  4063  nlim0  4286  snnex  4339  onsucelsucexmid  4415  0nelxp  4537  dm0  4723  iprc  4777  co02  5022  0fv  5424  frec0g  6262  nnsucuniel  6359  1nen2  6723  fidcenumlemrk  6810  djulclb  6908  ismkvnex  6997  0nnq  7140  0npr  7259  nqprdisj  7320  0ncn  7607  axpre-ltirr  7658  pnfnre  7775  mnfnre  7776  inelr  8314  xrltnr  9534  fzo0  9913  fzouzdisj  9925  inftonninf  10182  hashinfom  10492  3prm  11736  sqrt2irr  11767  ennnfonelem1  11847  bj-nndcALT  12890  bj-vprc  13021  pwle2  13120  exmidsbthrlem  13144
  Copyright terms: Public domain W3C validator