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

Theorem pm2.65i 168
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 115 . 2  |-  ( ps 
->  -.  ph )
3 pm2.65i.1 . . 3  |-  ( ph  ->  ps )
43con3i 130 . 2  |-  ( -. 
ps  ->  -.  ph )
52, 4pm2.61i 159 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mto  170  mt2  173  noel  3634  0nelop  4448  canth  6541  sdom0  7241  canthwdom  7549  cardprclem  7868  ominf4  8194  canthp1lem2  8530  pwfseqlem4  8539  pwxpndom2  8542  lbioo  10949  ubioo  10950  fzp1disj  11107  fzonel  11154  fzouzdisj  11171  hashbclem  11703  harmonic  12640  eirrlem  12805  ruclem13  12843  prmreclem6  13291  4sqlem17  13331  vdwlem12  13362  vdwnnlem3  13367  mreexmrid  13870  efgredlemb  15380  efgredlem  15381  00lss  16020  alexsublem  18077  ptcmplem4  18088  nmoleub2lem3  19125  dvferm1lem  19870  dvferm2lem  19872  plyeq0lem  20131  logno1  20529  lgsval2lem  21092  pntpbnd2  21283  ubico  24140  psgnunilem3  27398  bnj1523  29502
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator