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

Theorem pm2.65i 197
 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 141 . 2 (𝜓 → ¬ 𝜑)
3 pm2.65i.1 . . 3 (𝜑𝜓)
43con3i 157 . 2 𝜓 → ¬ 𝜑)
52, 4pm2.61i 185 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  198  mto  200  mt2  203  0nelop  5354  canth  7097  sdom0  8648  canthwdom  9042  cardprclem  9407  ominf4  9738  canthp1lem2  10079  pwfseqlem4  10088  pwxpndom2  10091  lbioo  12774  ubioo  12775  fzp1disj  12978  fzonel  13063  fzouzdisj  13085  hashbclem  13823  harmonic  15223  eirrlem  15566  ruclem13  15604  prmreclem6  16264  4sqlem17  16304  vdwlem12  16335  vdwnnlem3  16340  mreexmrid  16923  psgnunilem3  18634  efgredlemb  18882  efgredlem  18883  00lss  19724  alexsublem  22687  ptcmplem4  22698  nmoleub2lem3  23758  dvferm1lem  24625  dvferm2lem  24627  plyeq0lem  24848  logno1  25268  lgsval2lem  25932  pntpbnd2  26212  ubico  30565  bnj1523  32516  sn-inelr  39677  pm2.65ni  41765  lbioc  42234  salgencntex  43067
 Copyright terms: Public domain W3C validator