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  369  bija  370  con3dimp  457  aleximi  1757  nelcon3d  2906  rexim  3005  spcimegf  3282  spcimedv  3287  rspcimedv  3306  ssneld  3597  sscon  3736  difrab  3893  eqoreldifOLD  4217  disjord  4632  disjiund  4634  dtru  4848  otiunsndisj  4970  wereu2  5101  ndmfv  6205  dff3  6358  soisores  6562  ressuppssdif  7301  wfrlem10  7409  tz7.49  7525  oaord  7612  oalimcl  7625  omord2  7632  omcan  7634  omeulem1  7647  oeord  7653  oecan  7654  nnaord  7684  nnmord  7697  nneob  7717  omsmo  7719  domtriord  8091  isinf  8158  pssnn  8163  frfi  8190  fisupg  8193  difinf  8215  supmo  8343  infmo  8386  fiinfg  8390  alephord  8883  fin17  9201  isfin7-2  9203  fin1a2lem12  9218  fpwwe2lem13  9449  prub  9801  genpnnp  9812  ltaddpr  9841  prlem936  9854  ltadd2  10126  ltord1  10539  prodge0  10855  ltmul1  10858  lt2msq  10893  nnge1  11031  nzadd  11410  zeo  11448  irradd  11797  irrmul  11798  mul2lt0bi  11921  supxrun  12131  supxrgtmnf  12144  ssfzoulel  12546  zesq  12970  bccmpl  13079  fundmge2nop0  13257  repswswrd  13512  s3iunsndisj  13688  lcmftp  15330  prm2orodd  15385  coprm  15404  prmndvdsfaclt  15416  hashgcdeq  15475  prmreclem3  15603  vdwnnlem2  15681  latnlej2  17052  mgm2nsgrplem3  17388  f1omvdco2  17849  oddvds  17947  gexdvds  17980  frgpnabl  18259  ablfac1eulem  18452  ablfac1eu  18453  psgnodpm  19915  obselocv  20053  1marepvmarrepid  20362  mdetunilem9  20407  t1connperf  21220  txindislem  21417  fbasrn  21669  isufil2  21693  ufileu  21704  filufint  21705  ufilen  21715  fin1aufil  21717  alexsubALTlem4  21835  ptcmplem2  21838  itg2gt0  23508  cosord  24259  argimgt0  24339  logdivlt  24348  logrec  24482  dcubic  24554  wilthlem2  24776  bposlem3  24992  dchrisum0fno1  25181  numedglnl  26020  nbumgr  26224  uhgrnbgr0nb  26231  cusgrfi  26335  vtxduhgr0nedg  26369  uhgrvd00  26411  wlkp1lem6  26556  2wspmdisj  27175  chnlen0  28273  staddi  29075  stadd3i  29077  strlem1  29079  atoml2i  29212  psgnfzto1stlem  29824  madjusmdetlem1  29867  madjusmdetlem2  29868  hasheuni  30121  sitgaddlemb  30384  eulerpartlemb  30404  ballotlemfc0  30528  ballotlemfcc  30529  funeldmb  31637  dfon2lem6  31667  exnel  31682  sltres  31789  nosepssdm  31810  nosupbnd1lem1  31828  sletr  31857  nn0prpwlem  32292  waj-ax  32388  bj-dtru  32772  sucneqond  33184  wl-spae  33277  wl-ax11-lem3  33335  matunitlindflem1  33376  poimirlem26  33406  poimirlem28  33408  poimirlem31  33411  areacirc  33476  pridlc3  33843  lkreqN  34276  atlrelat1  34427  2llnneN  34514  cdlemg4c  35719  mapdh8e  36892  vk15.4j  38554  isosctrlem1ALT  38990  afvres  41015  otiunsndisjX  41061  fmtnoinf  41213  copisnmnd  41574  dig1  42167
  Copyright terms: Public domain W3C validator