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  2246  necon3ad  2495  necon2bd  2508  necon4ad  2520  spcimegf  2875  spcegf  2877  spcimedv  2880  rspcimedv  2899  minel  3523  disjxun  4037  sotric  4356  sotrieq  4357  onnminsb  4611  oneqmin  4612  ordunisuc2  4651  limsssuc  4657  poirr2  5083  funun  5312  imadif  5343  soisoi  5841  tz7.48lem  6469  sdomdif  7025  pssinf  7089  unblem1  7125  supnub  7229  elirrv  7327  inf3lem6  7350  cantnflem1  7407  cardne  7614  cardsdomel  7623  carddom2  7626  cardmin2  7647  alephnbtwn  7714  infdif2  7852  fin4en1  7951  fin23lem31  7985  isf32lem5  7999  isf34lem4  8019  cfpwsdom  8222  fpwwe2  8281  addnidpi  8541  genpnnp  8645  btwnnz  10104  prime  10108  qsqueeze  10544  xralrple  10548  xmullem2  10601  xmulneg1  10605  bcval4  11336  seqcoll  11417  fsumcvg  12201  fsumsplit  12228  dvdsle  12590  divalglem8  12615  bitsinv1lem  12648  pockthg  12969  prmunb  12977  vdwlem6  13049  ramlb  13082  gsumzsplit  15222  opsrtoslem2  16242  obselocv  16644  elcls  16826  fbasrn  17595  ufilb  17617  ufilmax  17618  rnelfmlem  17663  alexsubALTlem4  17760  tsmssplit  17850  recld2  18336  fsumharmonic  20321  chtub  20467  lgsne0  20588  cvnsym  22886  cvntr  22888  atcvati  22982  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemfrcn0  23104  ballotlemirc  23106  eupath2lem3  23918  fprodcvg  24153  dfpo2  24183  wfrlem10  24336  sltres  24389  nodenselem5  24410  nocvxminlem  24415  nobndup  24425  nobnddown  24426  nofulllem5  24431  axlowdim  24661  onsucconi  24948  onint1  24960  nn0prpw  26342  fdc  26558  rencldnfilem  27006  stoweidlem34  27886  hashtpg  28217  nbusgra  28277  nbgranself  28283  cyclnspth  28376  lsatcvat  29862  hlrelat2  30214  ltltncvr  30234  islln2a  30328  islpln2a  30359  islvol2aN  30403
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator