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

Theorem pm2.65i 167
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 114 . 2  |-  ( ps 
->  -.  ph )
3 pm2.65i.1 . . 3  |-  ( ph  ->  ps )
43con3i 129 . 2  |-  ( -. 
ps  ->  -.  ph )
52, 4pm2.61i 158 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mto  169  mt2  172  noel  3592  0nelop  4406  canth  6498  sdom0  7198  canthwdom  7503  cardprclem  7822  ominf4  8148  canthp1lem2  8484  pwfseqlem4  8493  pwxpndom2  8496  lbioo  10903  ubioo  10904  fzp1disj  11061  fzonel  11107  fzouzdisj  11124  hashbclem  11656  harmonic  12593  eirrlem  12758  ruclem13  12796  prmreclem6  13244  4sqlem17  13284  vdwlem12  13315  vdwnnlem3  13320  mreexmrid  13823  efgredlemb  15333  efgredlem  15334  00lss  15973  alexsublem  18028  ptcmplem4  18039  nmoleub2lem3  19076  dvferm1lem  19821  dvferm2lem  19823  plyeq0lem  20082  logno1  20480  lgsval2lem  21043  pntpbnd2  21234  ubico  24091  psgnunilem3  27287  bnj1523  29146
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator