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

Theorem pm2.65da 560
Description: Deduction rule for proof by contradiction. (Contributed by NM, 12-Jun-2014.)
Hypotheses
Ref Expression
pm2.65da.1  |-  ( (
ph  /\  ps )  ->  ch )
pm2.65da.2  |-  ( (
ph  /\  ps )  ->  -.  ch )
Assertion
Ref Expression
pm2.65da  |-  ( ph  ->  -.  ps )

Proof of Theorem pm2.65da
StepHypRef Expression
1 pm2.65da.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21ex 424 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.65da.2 . . 3  |-  ( (
ph  /\  ps )  ->  -.  ch )
43ex 424 . 2  |-  ( ph  ->  ( ps  ->  -.  ch ) )
52, 4pm2.65d 168 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359
This theorem is referenced by:  condan  770  nelrdva  3143  onnseq  6606  oeeulem  6844  disjen  7264  cantnflem1  7645  ssfin4  8190  fin1a2lem12  8291  fin1a2lem13  8292  canthnumlem  8523  canthwelem  8525  supmul1  9973  ixxdisj  10931  ixxub  10937  ixxlb  10938  icodisj  11022  discr1  11515  sqrlem7  12054  bitsfzolem  12946  bitsfzo  12947  sqnprm  13098  mreexexlem2d  13870  acsinfd  14606  lbsextlem3  16232  lbsextlem4  16233  iuncon  17491  ptcmplem4  18086  iccntr  18852  evth  18984  bcthlem5  19281  ovolicopnf  19420  vitalilem4  19503  dvferm1  19869  dvferm2  19871  dgreq0  20183  radcnvle  20336  isosctrlem2  20663  mersenne  21011  pntlem3  21303  ostth2lem1  21312  ex-natded5.5  21718  ex-natded5.8  21721  ex-natded5.13  21723  qqhre  24386  ballotlemfc0  24750  ballotlemfcc  24751  ballotlemimin  24763  ballotlem1c  24765  dmlogdmgm  24808  supaddc  26237  iunconlem2  29047  bnj1417  29410
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator