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

Theorem mtbir 671
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 670 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 614  ax-in2 615
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  nnexmid  850  nndc  851  fal  1360  ax-9  1531  nonconne  2359  nemtbir  2436  ru  2961  noel  3426  iun0  3940  0iun  3941  br0  4048  vprc  4132  iin0r  4166  nlim0  4391  snnex  4445  onsucelsucexmid  4526  0nelxp  4651  dm0  4837  iprc  4891  co02  5138  0fv  5546  frec0g  6392  nnsucuniel  6490  1nen2  6855  fidcenumlemrk  6947  djulclb  7048  ismkvnex  7147  pw1ne3  7223  sucpw1nel3  7226  3nsssucpw1  7229  0nnq  7351  0npr  7470  nqprdisj  7531  0ncn  7818  axpre-ltirr  7869  pnfnre  7986  mnfnre  7987  inelr  8528  xrltnr  9763  fzo0  10151  fzouzdisj  10163  inftonninf  10424  hashinfom  10739  3prm  12108  sqrt2irr  12142  ennnfonelem1  12388  bj-nndcALT  14159  bj-vprc  14297  pwle2  14397  exmidsbthrlem  14419
  Copyright terms: Public domain W3C validator