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

Theorem pm2.65i 185
 Description: Inference rule 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 136 . 2 (𝜓 → ¬ 𝜑)
3 pm2.65i.1 . . 3 (𝜑𝜓)
43con3i 151 . 2 𝜓 → ¬ 𝜑)
52, 4pm2.61i 176 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  186  mto  188  mt2  191  noel  4067  0nelop  5087  canth  6751  sdom0  8248  canthwdom  8640  cardprclem  9005  ominf4  9336  canthp1lem2  9677  pwfseqlem4  9686  pwxpndom2  9689  lbioo  12411  ubioo  12412  fzp1disj  12606  fzonel  12691  fzouzdisj  12712  hashbclem  13438  harmonic  14798  eirrlem  15138  ruclem13  15177  prmreclem6  15832  4sqlem17  15872  vdwlem12  15903  vdwnnlem3  15908  mreexmrid  16511  psgnunilem3  18123  efgredlemb  18366  efgredlem  18367  00lss  19152  alexsublem  22068  ptcmplem4  22079  nmoleub2lem3  23134  dvferm1lem  23967  dvferm2lem  23969  plyeq0lem  24186  logno1  24603  lgsval2lem  25253  pntpbnd2  25497  ubico  29877  bnj1523  31477  pm2.65ni  39731  lbioc  40258  salgencntex  41078
 Copyright terms: Public domain W3C validator