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

Theorem con2d 107
Description: A contraposition deduction. (Contributed by NM, 19-Aug-1993.)
Hypothesis
Ref Expression
con2d.1  |-  ( ph  ->  ( ps  ->  -.  ch ) )
Assertion
Ref Expression
con2d  |-  ( ph  ->  ( ch  ->  -.  ps ) )

Proof of Theorem con2d
StepHypRef Expression
1 notnot2 104 . . 3  |-  ( -. 
-.  ps  ->  ps )
2 con2d.1 . . 3  |-  ( ph  ->  ( ps  ->  -.  ch ) )
31, 2syl5 28 . 2  |-  ( ph  ->  ( -.  -.  ps  ->  -.  ch ) )
43con4d 97 1  |-  ( ph  ->  ( ch  ->  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  con2  108  mt2d  109  pm3.2im  137  exists2  2235  necon3ad  2484  necon2bd  2497  necon4ad  2509  spcimegf  2864  spcegf  2866  spcimedv  2869  rspcimedv  2888  minel  3512  disjxun  4023  sotric  4342  sotrieq  4343  onnminsb  4597  oneqmin  4598  ordunisuc2  4637  limsssuc  4643  poirr2  5069  funun  5298  imadif  5329  soisoi  5827  tz7.48lem  6455  sdomdif  7011  pssinf  7075  unblem1  7111  supnub  7215  elirrv  7313  inf3lem6  7336  cantnflem1  7393  cardne  7600  cardsdomel  7609  carddom2  7612  cardmin2  7633  alephnbtwn  7700  infdif2  7838  fin4en1  7937  fin23lem31  7971  isf32lem5  7985  isf34lem4  8005  cfpwsdom  8208  fpwwe2  8267  addnidpi  8527  genpnnp  8631  btwnnz  10090  prime  10094  qsqueeze  10530  xralrple  10534  xmullem2  10587  xmulneg1  10591  bcval4  11322  seqcoll  11403  fsumcvg  12187  fsumsplit  12214  dvdsle  12576  divalglem8  12601  bitsinv1lem  12634  pockthg  12955  prmunb  12963  vdwlem6  13035  ramlb  13068  gsumzsplit  15208  opsrtoslem2  16228  obselocv  16630  elcls  16812  fbasrn  17581  ufilb  17603  ufilmax  17604  rnelfmlem  17649  alexsubALTlem4  17746  tsmssplit  17836  recld2  18322  fsumharmonic  20307  chtub  20453  lgsne0  20574  cvnsym  22872  cvntr  22874  atcvati  22968  ballotlemfc0  23053  ballotlemfcc  23054  ballotlemfrcn0  23090  ballotlemirc  23092  eupath2lem3  23905  dfpo2  24114  wfrlem10  24267  sltres  24320  nodenselem5  24341  nocvxminlem  24346  nobndup  24356  nobnddown  24357  nofulllem5  24362  axlowdim  24591  onsucconi  24878  onint1  24890  nn0prpw  26250  fdc  26466  rencldnfilem  26914  stoweidlem34  27794  nbusgra  28154  nbgranself  28160  lsatcvat  29313  hlrelat2  29665  ltltncvr  29685  islln2a  29779  islpln2a  29810  islvol2aN  29854
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator