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

Theorem con3d 148
Description: A contraposition deduction. Deduction form of con3 149. (Contributed by NM, 10-Jan-1993.)
Hypothesis
Ref Expression
con3d.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
con3d (𝜑 → (¬ 𝜒 → ¬ 𝜓))

Proof of Theorem con3d
StepHypRef Expression
1 notnotr 125 . . 3 (¬ ¬ 𝜓𝜓)
2 con3d.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2syl5 34 . 2 (𝜑 → (¬ ¬ 𝜓𝜒))
43con1d 139 1 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  con3  149  con3rr3  151  nsyld  154  nsyli  155  mth8  158  pm2.52  167  pm5.21ndd  368  bija  369  con3dimp  456  aleximi  1799  nelcon3d  2938  rexim  3037  spcimegf  3318  spcimedv  3323  rspcimedv  3342  ssneld  3638  sscon  3777  difrab  3934  eqoreldifOLD  4258  disjord  4673  disjiund  4675  dtru  4887  otiunsndisj  5009  wereu2  5140  ndmfv  6256  dff3  6412  soisores  6617  ressuppssdif  7361  wfrlem10  7469  tz7.49  7585  oaord  7672  oalimcl  7685  omord2  7692  omcan  7694  omeulem1  7707  oeord  7713  oecan  7714  nnaord  7744  nnmord  7757  nneob  7777  omsmo  7779  domtriord  8147  isinf  8214  pssnn  8219  frfi  8246  fisupg  8249  difinf  8271  supmo  8399  infmo  8442  fiinfg  8446  alephord  8936  fin17  9254  isfin7-2  9256  fin1a2lem12  9271  fpwwe2lem13  9502  prub  9854  genpnnp  9865  ltaddpr  9894  prlem936  9907  ltadd2  10179  ltord1  10592  prodge0  10908  ltmul1  10911  lt2msq  10946  nnge1  11084  nzadd  11463  zeo  11501  irradd  11850  irrmul  11851  mul2lt0bi  11974  supxrun  12184  supxrgtmnf  12197  ssfzoulel  12602  zesq  13027  bccmpl  13136  fundmge2nop0  13312  repswswrd  13577  s3iunsndisj  13753  lcmftp  15396  prm2orodd  15451  coprm  15470  prmndvdsfaclt  15482  hashgcdeq  15541  prmreclem3  15669  vdwnnlem2  15747  latnlej2  17118  mgm2nsgrplem3  17454  f1omvdco2  17914  oddvds  18012  gexdvds  18045  frgpnabl  18324  ablfac1eulem  18517  ablfac1eu  18518  psgnodpm  19982  obselocv  20120  1marepvmarrepid  20429  mdetunilem9  20474  t1connperf  21287  txindislem  21484  fbasrn  21735  isufil2  21759  ufileu  21770  filufint  21771  ufilen  21781  fin1aufil  21783  alexsubALTlem4  21901  ptcmplem2  21904  itg2gt0  23572  cosord  24323  argimgt0  24403  logdivlt  24412  logrec  24546  dcubic  24618  wilthlem2  24840  bposlem3  25056  dchrisum0fno1  25245  numedglnl  26084  nbumgr  26288  uhgrnbgr0nb  26295  cusgrfi  26410  vtxduhgr0nedg  26444  uhgrvd00  26486  wlkp1lem6  26631  2wspmdisj  27317  chnlen0  28431  staddi  29233  stadd3i  29235  strlem1  29237  atoml2i  29370  psgnfzto1stlem  29978  madjusmdetlem1  30021  madjusmdetlem2  30022  hasheuni  30275  sitgaddlemb  30538  eulerpartlemb  30558  ballotlemfc0  30682  ballotlemfcc  30683  funeldmb  31787  dfon2lem6  31817  exnel  31832  frpomin  31863  sltres  31940  nosepssdm  31961  nosupbnd1lem1  31979  sletr  32008  nn0prpwlem  32442  waj-ax  32538  bj-dtru  32922  sucneqond  33343  wl-spae  33436  wl-ax11-lem3  33494  matunitlindflem1  33535  poimirlem26  33565  poimirlem28  33567  poimirlem31  33570  areacirc  33635  pridlc3  34002  lkreqN  34775  atlrelat1  34926  2llnneN  35013  cdlemg4c  36217  mapdh8e  37390  vk15.4j  39051  isosctrlem1ALT  39484  afvres  41573  otiunsndisjX  41621  fmtnoinf  41773  copisnmnd  42134  dig1  42727
  Copyright terms: Public domain W3C validator