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

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

Proof of Theorem con3d
StepHypRef Expression
1 notnotr 123 . . 3 (¬ ¬ 𝜓𝜓)
2 con3d.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2syl5 33 . 2 (𝜑 → (¬ ¬ 𝜓𝜒))
43con1d 137 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  147  con3rr3  149  nsyld  152  nsyli  153  mth8  156  pm2.52  165  pm5.21ndd  367  bija  368  con3dimp  455  aleximi  1748  nelcon3d  2894  rexim  2990  spcimegf  3259  spcimedv  3264  rspcimedv  3283  ssneld  3569  sscon  3705  difrab  3859  eqoreldifOLD  4172  dtru  4778  otiunsndisj  4896  wereu2  5025  ndmfv  6113  dff3  6265  soisores  6455  ressuppssdif  7180  wfrlem10  7288  tz7.49  7404  oaord  7491  oalimcl  7504  omord2  7511  omcan  7513  omeulem1  7526  oeord  7532  oecan  7533  nnaord  7563  nnmord  7576  nneob  7596  omsmo  7598  domtriord  7968  isinf  8035  pssnn  8040  frfi  8067  fisupg  8070  difinf  8092  supmo  8218  infmo  8261  fiinfg  8265  alephord  8758  fin17  9076  isfin7-2  9078  fin1a2lem12  9093  fpwwe2lem13  9320  prub  9672  genpnnp  9683  ltaddpr  9712  prlem936  9725  ltadd2  9992  ltord1  10403  prodge0  10719  ltmul1  10722  lt2msq  10757  nnge1  10893  nzadd  11258  zeo  11295  irradd  11644  irrmul  11645  mul2lt0bi  11768  supxrun  11974  supxrgtmnf  11987  ssfzoulel  12383  zesq  12804  bccmpl  12913  repswswrd  13328  s3iunsndisj  13501  lcmftp  15133  prm2orodd  15188  coprm  15207  prmndvdsfaclt  15219  hashgcdeq  15278  prmreclem3  15406  vdwnnlem2  15484  latnlej2  16840  mgm2nsgrplem3  17176  f1omvdco2  17637  oddvds  17735  gexdvds  17768  frgpnabl  18047  ablfac1eulem  18240  ablfac1eu  18241  psgnodpm  19698  obselocv  19833  1marepvmarrepid  20142  mdetunilem9  20187  t1conperf  20991  txindislem  21188  fbasrn  21440  isufil2  21464  ufileu  21475  filufint  21476  ufilen  21486  fin1aufil  21488  alexsubALTlem4  21606  ptcmplem2  21609  itg2gt0  23250  cosord  23999  argimgt0  24079  logdivlt  24088  logrec  24218  dcubic  24290  wilthlem2  24512  bposlem3  24728  dchrisum0fno1  24917  usgranloop0  25675  nbgra0nb  25724  nbcusgra  25758  cusgrafi  25776  vdusgra0nedg  26201  usgravd0nedg  26211  usgravd00  26212  2spotmdisj  26361  chnlen0  27493  staddi  28295  stadd3i  28297  strlem1  28299  atoml2i  28432  psgnfzto1stlem  28987  madjusmdetlem1  29027  madjusmdetlem2  29028  hasheuni  29280  sitgaddlemb  29543  eulerpartlemb  29563  ballotlemfc0  29687  ballotlemfcc  29688  dfon2lem6  30743  exnel  30758  sltres  30867  nodenselem4  30889  nofulllem5  30911  nn0prpwlem  31293  waj-ax  31389  bj-dtru  31791  sucneqond  32185  wl-spae  32281  wl-ax11-lem3  32339  matunitlindflem1  32371  poimirlem26  32401  poimirlem28  32403  poimirlem31  32406  areacirc  32471  pridlc3  32838  lkreqN  33271  atlrelat1  33422  2llnneN  33509  cdlemg4c  34714  mapdh8e  35887  vk15.4j  37551  isosctrlem1ALT  37988  afvres  39699  fmtnoinf  39784  otiunsndisjX  40125  fundmge2nop0  40145  nbumgr  40564  uhgrnbgr0nb  40571  cusgrfi  40669  vtxduhgr0nedg  40702  uhgrvd00  40745  1wlkp1lem6  40882  2wspdisj  41160  2wspmdisj  41496  copisnmnd  41594  dig1  42195
  Copyright terms: Public domain W3C validator