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  1294  ax-9  1467  nonconne  2263  nemtbir  2340  ru  2828  noel  3279  iun0  3771  0iun  3772  vprc  3948  iin0r  3981  nlim0  4197  snnex  4247  onsucelsucexmid  4321  0nelxp  4440  dm0  4620  iprc  4671  co02  4912  0fv  5304  frec0g  6118  nnsucuniel  6212  1nen2  6531  djulclb  6694  0nnq  6870  0npr  6989  nqprdisj  7050  0ncn  7316  axpre-ltirr  7364  pnfnre  7476  mnfnre  7477  inelr  8005  xrltnr  9185  fzo0  9510  fzouzdisj  9522  inftonninf  9778  hashinfom  10086  3prm  11016  sqrt2irr  11047  nnexmid  11129  nndc  11130  bj-vprc  11256  exmidsbthrlem  11381
  Copyright terms: Public domain W3C validator