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

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

Proof of Theorem con3d
StepHypRef Expression
1 notnot2 104 . . 3  |-  ( -. 
-.  ps  ->  ps )
2 con3d.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 28 . 2  |-  ( ph  ->  ( -.  -.  ps  ->  ch ) )
43con1d 116 1  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  con3  126  con3rr3  128  nsyld  132  nsyli  133  mth8  138  pm2.52  147  pm5.21ndd  343  bija  344  con3and  428  ax12bOLD  1656  ax12olem1  1868  spime  1916  mo  2165  necon1bd  2514  rexim  2647  spcimegf  2862  spcimedv  2867  rspcimedv  2886  ssneld  3182  sscon  3310  difrab  3442  dtru  4201  wereu2  4390  nsuceq0  4472  ndmfv  5552  dff3  5673  soisores  5824  tz7.49  6457  oaord  6545  oalimcl  6558  omord2  6565  omcan  6567  omeulem1  6580  oeord  6586  oecan  6587  nnaord  6617  nnmord  6630  nneob  6650  omsmo  6652  domtriord  7007  isinf  7076  pssnn  7081  frfi  7102  fisupg  7105  difinf  7127  supmo  7203  alephord  7702  kmlem2  7777  fin17  8020  isfin7-2  8022  fin1a2lem12  8037  fpwwe2lem13  8264  prub  8618  genpnnp  8629  ltaddpr  8658  prlem936  8671  ltadd2  8924  ltord1  9299  prodge0  9603  ltmul1  9606  lt2msq  9640  nnge1  9772  zeo  10097  irradd  10340  irrmul  10341  supxrun  10634  supxrgtmnf  10648  zesq  11224  bccmpl  11322  hashbclem  11390  coprm  12779  prmreclem3  12965  vdwnnlem2  13043  latnlej2  14177  oddvds  14862  gexdvds  14895  frgpnabl  15163  ablfac1eulem  15307  ablfac1eu  15308  obselocv  16628  t1conperf  17162  txindislem  17327  fbasrn  17579  isufil2  17603  ufileu  17614  filufint  17615  ufilen  17625  fin1aufil  17627  alexsubALTlem4  17744  ptcmplem2  17747  itg2gt0  19115  mpfrcl  19402  cosord  19894  argimgt0  19966  logdivlt  19972  logrec  20117  dcubic  20142  wilthlem2  20307  bposlem3  20525  dchrisum0fno1  20660  chnlen0  22023  staddi  22826  stadd3i  22828  strlem1  22830  atoml2i  22963  ifeqeqx  23034  ballotlemfc0  23051  ballotlemfcc  23052  xrge0npcan  23333  hasheuni  23453  dfon2lem6  24144  exnel  24159  wfrlem10  24265  sltres  24318  nodenselem4  24338  nofulllem5  24360  hfext  24813  waj-ax  24853  onsuct0  24880  areacirc  24931  diaimd  25010  fisub  25554  carinttar  25902  pdiveql  26168  nn0prpwlem  26238  pridlc3  26698  f1omvdco2  27391  hashgcdeq  27517  pm10.56  27565  afvres  28034  nbusgra  28143  nbgra0nb  28144  nbcusgra  28159  vk15.4j  28291  ax12-3  29104  a12stdy1-x12  29111  a12stdy1  29126  a12stdy4  29129  a12studyALT  29133  a12study10n  29137  ax9lem6  29145  ax9lem15  29154  ax9vax9  29158  lkreqN  29360  atlrelat1  29511  2llnneN  29598  cdlemg4c  30801  dvhdimlem  31634  dvh3dim2  31638  dvh3dim3N  31639  mapdh8e  31974  mapdh9a  31980  hdmapval0  32026  hdmap11lem2  32035
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator