MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.65i Structured version   Visualization version   GIF version

Theorem pm2.65i 186
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 (𝜑 → ¬ 𝜓)
21con2i 137 . 2 (𝜓 → ¬ 𝜑)
3 pm2.65i.1 . . 3 (𝜑𝜓)
43con3i 152 . 2 𝜓 → ¬ 𝜑)
52, 4pm2.61i 177 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  pm2.21dd  187  mto  189  mt2  192  noelOLD  4147  0nelop  5193  canth  6882  sdom0  8382  canthwdom  8775  cardprclem  9140  ominf4  9471  canthp1lem2  9812  pwfseqlem4  9821  pwxpndom2  9824  lbioo  12522  ubioo  12523  fzp1disj  12721  fzonel  12806  fzouzdisj  12827  hashbclem  13554  harmonic  14999  eirrlem  15340  ruclem13  15379  prmreclem6  16033  4sqlem17  16073  vdwlem12  16104  vdwnnlem3  16109  mreexmrid  16693  psgnunilem3  18304  efgredlemb  18548  efgredlem  18549  efgredlemOLD  18550  00lss  19338  alexsublem  22260  ptcmplem4  22271  nmoleub2lem3  23326  dvferm1lem  24188  dvferm2lem  24190  plyeq0lem  24407  logno1  24823  lgsval2lem  25488  pntpbnd2  25732  ubico  30105  bnj1523  31742  pm2.65ni  40152  lbioc  40658  salgencntex  41495
  Copyright terms: Public domain W3C validator