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  2307  necon3ad  2565  necon2bd  2578  necon4ad  2590  spcimegf  2947  spcegf  2949  spcimedv  2952  rspcimedv  2971  minel  3598  disjxun  4123  sotric  4443  sotrieq  4444  onnminsb  4698  oneqmin  4699  ordunisuc2  4738  limsssuc  4744  poirr2  5170  funun  5399  imadif  5432  soisoi  5948  tz7.48lem  6595  sdomdif  7152  pssinf  7216  unblem1  7256  supnub  7360  elirrv  7458  inf3lem6  7481  cantnflem1  7538  cardne  7745  cardsdomel  7754  carddom2  7757  cardmin2  7778  alephnbtwn  7845  infdif2  7983  fin4en1  8082  fin23lem31  8116  isf32lem5  8130  isf34lem4  8150  cfpwsdom  8353  fpwwe2  8412  addnidpi  8672  genpnnp  8776  btwnnz  10239  prime  10243  qsqueeze  10680  xralrple  10684  xmullem2  10737  xmulneg1  10741  elfznelfzob  11080  bcval4  11485  hashtpg  11578  seqcoll  11599  fsumcvg  12393  fsumsplit  12420  dvdsle  12782  divalglem8  12807  bitsinv1lem  12840  pockthg  13161  prmunb  13169  vdwlem6  13241  ramlb  13274  gsumzsplit  15416  opsrtoslem2  16436  obselocv  16845  elcls  17027  fbasrn  17792  ufilb  17814  ufilmax  17815  rnelfmlem  17860  alexsubALTlem4  17957  tsmssplit  18047  recld2  18533  fsumharmonic  20528  chtub  20674  lgsne0  20795  cvnsym  23183  cvntr  23185  atcvati  23279  ballotlemfc0  24198  ballotlemfcc  24199  ballotlemfrcn0  24235  ballotlemirc  24237  eupath2lem3  24490  fprodcvg  24740  fprodsplit  24773  dfpo2  24853  wfrlem10  25006  sltres  25059  nodenselem5  25080  nocvxminlem  25085  nobndup  25095  nobnddown  25096  nofulllem5  25101  axlowdim  25331  onsucconi  25618  onint1  25630  nn0prpw  25746  fdc  25962  rencldnfilem  26409  stoweidlem34  27289  nbusgra  27596  nbgranself  27602  usgrasscusgra  27648  cyclnspth  27756  lsatcvat  29311  hlrelat2  29663  ltltncvr  29683  islln2a  29777  islpln2a  29808  islvol2aN  29852
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator