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  1675  ax12olem1  1880  spime  1929  mo  2178  necon1bd  2527  rexim  2660  spcimegf  2875  spcimedv  2880  rspcimedv  2899  ssneld  3195  sscon  3323  difrab  3455  dtru  4217  wereu2  4406  nsuceq0  4488  ndmfv  5568  dff3  5689  soisores  5840  tz7.49  6473  oaord  6561  oalimcl  6574  omord2  6581  omcan  6583  omeulem1  6596  oeord  6602  oecan  6603  nnaord  6633  nnmord  6646  nneob  6666  omsmo  6668  domtriord  7023  isinf  7092  pssnn  7097  frfi  7118  fisupg  7121  difinf  7143  supmo  7219  alephord  7718  kmlem2  7793  fin17  8036  isfin7-2  8038  fin1a2lem12  8053  fpwwe2lem13  8280  prub  8634  genpnnp  8645  ltaddpr  8674  prlem936  8687  ltadd2  8940  ltord1  9315  prodge0  9619  ltmul1  9622  lt2msq  9656  nnge1  9788  zeo  10113  irradd  10356  irrmul  10357  supxrun  10650  supxrgtmnf  10664  zesq  11240  bccmpl  11338  hashbclem  11406  coprm  12795  prmreclem3  12981  vdwnnlem2  13059  latnlej2  14193  oddvds  14878  gexdvds  14911  frgpnabl  15179  ablfac1eulem  15323  ablfac1eu  15324  obselocv  16644  t1conperf  17178  txindislem  17343  fbasrn  17595  isufil2  17619  ufileu  17630  filufint  17631  ufilen  17641  fin1aufil  17643  alexsubALTlem4  17760  ptcmplem2  17763  itg2gt0  19131  mpfrcl  19418  cosord  19910  argimgt0  19982  logdivlt  19988  logrec  20133  dcubic  20158  wilthlem2  20323  bposlem3  20541  dchrisum0fno1  20676  chnlen0  22039  staddi  22842  stadd3i  22844  strlem1  22846  atoml2i  22979  ifeqeqx  23050  ballotlemfc0  23067  ballotlemfcc  23068  xrge0npcan  23348  hasheuni  23468  dfon2lem6  24215  exnel  24230  wfrlem10  24336  sltres  24389  nodenselem4  24409  nofulllem5  24431  hfext  24885  waj-ax  24925  onsuct0  24952  areacirc  25034  diaimd  25113  fisub  25657  carinttar  26005  pdiveql  26271  nn0prpwlem  26341  pridlc3  26801  f1omvdco2  27494  hashgcdeq  27620  pm10.56  27668  afvres  28140  nbusgra  28277  nbgra0nb  28278  nbcusgra  28298  vk15.4j  28590  spimeNEW7  29486  ax12-3  29726  a12stdy1-x12  29733  a12stdy1  29748  a12stdy4  29751  a12studyALT  29755  a12study10n  29759  ax9lem6  29767  ax9lem15  29776  ax9vax9  29780  lkreqN  29982  atlrelat1  30133  2llnneN  30220  cdlemg4c  31423  dvhdimlem  32256  dvh3dim2  32260  dvh3dim3N  32261  mapdh8e  32596  mapdh9a  32602  hdmapval0  32648  hdmap11lem2  32657
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator