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

Theorem con3d 133
Description: A contraposition deduction. Deduction form of con3 134. (Contributed by NM, 10-Jan-1993.)
Hypothesis
Ref Expression
con3d.1
Assertion
Ref Expression
con3d

Proof of Theorem con3d
StepHypRef Expression
1 notnot2 112 . . 3
2 con3d.1 . . 3
31, 2syl5 32 . 2
43con1d 124 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  con3  134  con3rr3  136  nsyld  140  nsyli  141  mth8  146  pm2.52  155  pm5.21ndd  354  bija  355  con3dimp  441  aleximi  1653  necon1bdOLD  2676  nelcon3d  2806  rexim  2922  spcimegf  3188  spcimedv  3193  rspcimedv  3212  ssneld  3505  sscon  3637  difrab  3771  dtru  4643  otiunsndisj  4758  wereu2  4881  nsuceq0  4963  ndmfv  5895  dff3  6044  soisores  6223  ressuppssdif  6940  tz7.49  7129  oaord  7215  oalimcl  7228  omord2  7235  omcan  7237  omeulem1  7250  oeord  7256  oecan  7257  nnaord  7287  nnmord  7300  nneob  7320  omsmo  7322  domtriord  7683  isinf  7753  pssnn  7758  frfi  7785  fisupg  7788  difinf  7810  supmo  7932  alephord  8477  fin17  8795  isfin7-2  8797  fin1a2lem12  8812  fpwwe2lem13  9041  prub  9393  genpnnp  9404  ltaddpr  9433  prlem936  9446  ltadd2  9709  ltord1  10104  prodge0  10414  ltmul1  10417  lt2msq  10454  nnge1  10587  zeo  10973  irradd  11235  irrmul  11236  supxrun  11536  supxrgtmnf  11550  ssfzoulel  11906  zesq  12289  bccmpl  12387  swrd0  12658  repswswrd  12756  coprm  14241  prmreclem3  14436  vdwnnlem2  14514  latnlej2  15701  mgm2nsgrplem3  16038  f1omvdco2  16473  oddvds  16571  gexdvds  16604  frgpnabl  16879  ablfac1eulem  17123  ablfac1eu  17124  psgnodpm  18624  obselocv  18759  1marepvmarrepid  19077  mdetunilem9  19122  t1conperf  19937  txindislem  20134  fbasrn  20385  isufil2  20409  ufileu  20420  filufint  20421  ufilen  20431  fin1aufil  20433  alexsubALTlem4  20550  ptcmplem2  20553  itg2gt0  22167  cosord  22919  argimgt0  22997  logdivlt  23006  logrec  23151  dcubic  23177  wilthlem2  23343  bposlem3  23561  dchrisum0fno1  23696  usgranloop0  24380  nbgra0nb  24429  nbcusgra  24463  cusgrafi  24482  vdusgra0nedg  24908  usgravd0nedg  24918  usgravd00  24919  2spotmdisj  25068  chnlen0  26362  staddi  27165  stadd3i  27167  strlem1  27169  atoml2i  27302  mul2lt0bi  27569  hasheuni  28091  eulerpartlemb  28307  ballotlemfc0  28431  ballotlemfcc  28432  dfon2lem6  29220  exnel  29235  wfrlem10  29352  sltres  29424  nodenselem4  29444  nofulllem5  29466  waj-ax  29879  wl-ax11-lem3  30027  areacirc  30112  nn0prpwlem  30140  pridlc3  30470  hashgcdeq  31158  afvres  32257  otiunsndisjX  32301  copisnmnd  32497  vk15.4j  33298  isosctrlem1ALT  33734  bj-dtru  34383  lkreqN  34895  atlrelat1  35046  2llnneN  35133  cdlemg4c  36338  mapdh8e  37511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator