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  2233  necon3ad  2482  necon2bd  2495  necon4ad  2507  spcimegf  2862  spcegf  2864  spcimedv  2867  rspcimedv  2886  minel  3510  disjxun  4021  sotric  4340  sotrieq  4341  onnminsb  4595  oneqmin  4596  ordunisuc2  4635  limsssuc  4641  poirr2  5067  funun  5296  imadif  5327  soisoi  5825  tz7.48lem  6453  sdomdif  7009  pssinf  7073  unblem1  7109  supnub  7213  elirrv  7311  inf3lem6  7334  cantnflem1  7391  cardne  7598  cardsdomel  7607  carddom2  7610  cardmin2  7631  alephnbtwn  7698  infdif2  7836  fin4en1  7935  fin23lem31  7969  isf32lem5  7983  isf34lem4  8003  cfpwsdom  8206  fpwwe2  8265  addnidpi  8525  genpnnp  8629  btwnnz  10088  prime  10092  qsqueeze  10528  xralrple  10532  xmullem2  10585  xmulneg1  10589  bcval4  11320  seqcoll  11401  fsumcvg  12185  fsumsplit  12212  dvdsle  12574  divalglem8  12599  bitsinv1lem  12632  pockthg  12953  prmunb  12961  vdwlem6  13033  ramlb  13066  gsumzsplit  15206  opsrtoslem2  16226  obselocv  16628  elcls  16810  fbasrn  17579  ufilb  17601  ufilmax  17602  rnelfmlem  17647  alexsubALTlem4  17744  tsmssplit  17834  recld2  18320  fsumharmonic  20305  chtub  20451  lgsne0  20572  cvnsym  22870  cvntr  22872  atcvati  22966  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemfrcn0  23088  ballotlemirc  23090  eupath2lem3  23314  dfpo2  23523  wfrlem10  23676  sltres  23729  nodenselem5  23750  nocvxminlem  23755  nobndup  23765  nobnddown  23766  nofulllem5  23771  axlowdim  24000  onsucconi  24287  onint1  24299  nn0prpw  25651  fdc  25867  rencldnfilem  26315  stoweidlem34  27195  lsatcvat  28613  hlrelat2  28965  ltltncvr  28985  islln2a  29079  islpln2a  29110  islvol2aN  29154
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator