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

Theorem pm2.65i 178
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  |-  ( ph  ->  ps )
pm2.65i.2  |-  ( ph  ->  -.  ps )
Assertion
Ref Expression
pm2.65i  |-  -.  ph

Proof of Theorem pm2.65i
StepHypRef Expression
1 pm2.65i.2 . . 3  |-  ( ph  ->  -.  ps )
21con2i 124 . 2  |-  ( ps 
->  -.  ph )
3 pm2.65i.1 . . 3  |-  ( ph  ->  ps )
43con3i 142 . 2  |-  ( -. 
ps  ->  -.  ph )
52, 4pm2.61i 169 1  |-  -.  ph
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  179  mto  181  mt2  184  noel  3726  0nelop  4691  canth  6267  sdom0  7722  canthwdom  8112  cardprclem  8431  ominf4  8760  canthp1lem2  9096  pwfseqlem4  9105  pwxpndom2  9108  lbioo  11692  ubioo  11693  fzp1disj  11880  fzonel  11960  fzouzdisj  11981  hashbclem  12656  harmonic  13994  eirrlem  14333  ruclem13  14371  prmreclem6  14944  4sqlem17OLD  14984  4sqlem17  14990  vdwlem12  15021  vdwnnlem3  15026  mreexmrid  15627  psgnunilem3  17215  efgredlemb  17474  efgredlem  17475  00lss  18243  alexsublem  21137  ptcmplem4  21148  nmoleub2lem3  22207  dvferm1lem  23015  dvferm2lem  23017  plyeq0lem  23243  logno1  23660  lgsval2lem  24313  pntpbnd2  24504  ubico  28432  bnj1523  29952  pm2.65ni  37438  lbioc  37710  salgencntex  38314
  Copyright terms: Public domain W3C validator