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

Theorem pm2.65i 640
Description: Inference for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
Hypotheses
Ref Expression
pm2.65i.1 (𝜑𝜓)
pm2.65i.2 (𝜑 → ¬ 𝜓)
Assertion
Ref Expression
pm2.65i ¬ 𝜑

Proof of Theorem pm2.65i
StepHypRef Expression
1 pm2.65i.2 . . 3 (𝜑 → ¬ 𝜓)
2 pm2.65i.1 . . 3 (𝜑𝜓)
31, 2nsyl3 627 . 2 (𝜑 → ¬ 𝜑)
4 pm2.01 617 . 2 ((𝜑 → ¬ 𝜑) → ¬ 𝜑)
53, 4ax-mp 5 1 ¬ 𝜑
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 615  ax-in2 616
This theorem is referenced by:  mt2  641  mto  663  pm5.19  707  noel  3441  0nelop  4266  elirr  4558  en2lp  4571  soirri  5041  canth  5849  0neqopab  5940  fzp1disj  10109  fzonel  10189  fzouzdisj  10209  4sqlem17  12438  lgsval2lem  14864  bj-imnimnn  14943  nnnotnotr  15195
  Copyright terms: Public domain W3C validator