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

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

Proof of Theorem con3d
StepHypRef Expression
1 notnotr 128 . . 3 (¬ ¬ 𝜓𝜓)
2 con3d.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2syl5 34 . 2 (𝜑 → (¬ ¬ 𝜓𝜒))
43con1d 141 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  150  con3rr3  152  nsyld  155  nsyli  156  mth8  159  pm2.52  168  pm5.21ndd  370  bija  371  con3dimp  397  orim12dALT  935  aleximi  1926  nelcon3d  3052  rexim  3154  spcimegf  3439  spcimedv  3444  rspcimedv  3463  ssneld  3763  sscon  3906  difrab  4065  disjord  4798  disjiund  4800  dtru  5006  otiunsndisj  5141  wereu2  5274  ndmfv  6405  dff3  6562  soisores  6769  ressuppssdif  7518  wfrlem10  7628  tz7.49  7744  oaord  7832  oalimcl  7845  omord2  7852  omcan  7854  omeulem1  7867  oeord  7873  oecan  7874  nnaord  7904  nnmord  7917  nneob  7937  omsmo  7939  domtriord  8313  isinf  8380  pssnn  8385  frfi  8412  fisupg  8415  difinf  8437  supmo  8565  infmo  8608  fiinfg  8612  alephord  9149  fin17  9469  isfin7-2  9471  fin1a2lem12  9486  fpwwe2lem13  9717  prub  10069  genpnnp  10080  ltaddpr  10109  prlem936  10122  ltadd2  10395  ltord1  10808  prodge0OLD  11124  ltmul1  11127  lt2msq  11162  nnge1  11303  nzadd  11672  zeo  11710  irradd  12013  irrmul  12014  mul2lt0bi  12134  supxrun  12348  supxrgtmnf  12361  ssfzoulel  12770  zesq  13194  bccmpl  13300  fundmge2nop0  13475  repswswrd  13808  s3iunsndisj  13994  lcmftp  15630  prm2orodd  15684  coprm  15702  prmndvdsfaclt  15714  hashgcdeq  15773  prmreclem3  15901  vdwnnlem2  15979  latnlej2  17337  mgm2nsgrplem3  17674  f1omvdco2  18131  oddvds  18230  gexdvds  18263  frgpnabl  18544  ablfac1eulem  18738  ablfac1eu  18739  psgnodpm  20206  obselocv  20348  1marepvmarrepid  20658  mdetunilem9  20703  t1connperf  21519  txindislem  21716  fbasrn  21967  isufil2  21991  ufileu  22002  filufint  22003  ufilen  22013  fin1aufil  22015  alexsubALTlem4  22133  ptcmplem2  22136  itg2gt0  23818  cosord  24570  argimgt0  24649  logdivlt  24658  logrec  24792  dcubic  24864  wilthlem2  25086  bposlem3  25302  dchrisum0fno1  25491  numedglnl  26317  nbumgr  26522  uhgrnbgr0nb  26529  cusgrfi  26645  vtxduhgr0nedg  26679  uhgrvd00  26721  wlkp1lem6  26867  2wspmdisj  27617  chnlen0  28759  staddi  29561  stadd3i  29563  strlem1  29565  atoml2i  29698  psgnfzto1stlem  30297  madjusmdetlem1  30340  madjusmdetlem2  30341  hasheuni  30594  sitgaddlemb  30857  eulerpartlemb  30877  ballotlemfc0  31002  ballotlemfcc  31003  funeldmb  32106  dfon2lem6  32136  exnel  32151  frpomin  32182  sltres  32259  nosepssdm  32280  nosupbnd1lem1  32298  sletr  32327  nn0prpwlem  32760  waj-ax  32852  bj-dtru  33227  sucneqond  33646  wl-spae  33733  wl-ax11-lem3  33789  matunitlindflem1  33829  poimirlem26  33859  poimirlem28  33861  poimirlem31  33864  areacirc  33928  pridlc3  34294  lkreqN  35126  atlrelat1  35277  2llnneN  35365  cdlemg4c  36568  mapdh8e  37740  vk15.4j  39406  isosctrlem1ALT  39822  afvres  41920  otiunsndisjX  42028  fmtnoinf  42124  copisnmnd  42478  dig1  43071
  Copyright terms: Public domain W3C validator