Theorem con3d 155

Description: A contraposition deduction. Deduction form of con3 156. (Contributed by NM, 10-Jan-1993.)

Hypothesis

Ref	Expression
con3d.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
con3d	⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))

Proof of Theorem con3d

Step	Hyp	Ref	Expression
1		notnotr 132	. . 3 ⊢ (¬ ¬ 𝜓 → 𝜓)
2		con3d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 34	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝜒))
4	3	con1d 147	1 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))

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  156  con3rr3  158  nsyld  159  nsyli  160  jcn  164  pm5.21ndd  383  bija  384  con3dimp  411  orim12dALT  908  aleximi  1832  nelcon3d  3135  rexim  3241  spcimegf  3589  spcimedv  3594  rspcimedv  3614  ssneld  3969  sscon  4115  difrab  4277  disjord  5054  disjiund  5056  dtru  5271  otiunsndisj  5410  wereu2  5552  ndmfv  6700  dff3  6866  soisores  7080  releldmdifi  7744  funeldmdif  7747  ressuppssdif  7851  wfrlem10  7964  tz7.49  8081  oaord  8173  oalimcl  8186  omord2  8193  omcan  8195  omeulem1  8208  oeord  8214  oecan  8215  nnaord  8245  nnmord  8258  nneob  8279  omsmo  8281  domtriord  8663  isinf  8731  pssnn  8736  frfi  8763  fisupg  8766  difinf  8788  supmo  8916  infmo  8959  alephord  9501  fin17  9816  isfin7-2  9818  fin1a2lem12  9833  fpwwe2lem13  10064  prub  10416  genpnnp  10427  ltaddpr  10456  prlem936  10469  ltadd2  10744  ltord1  11166  ltmul1  11490  lt2msq  11525  nnge1  11666  nzadd  12031  zeo  12069  irradd  12373  irrmul  12374  mul2lt0bi  12496  supxrun  12710  supxrgtmnf  12723  ssfzoulel  13132  zesq  13588  bccmpl  13670  fundmge2nop0  13851  repswswrd  14146  s3iunsndisj  14328  lcmftp  15980  prm2orodd  16035  coprm  16055  prmndvdsfaclt  16067  hashgcdeq  16126  prmreclem3  16254  vdwnnlem2  16332  latnlej2  17681  mgm2nsgrplem3  18085  f1omvdco2  18576  oddvds  18675  gexdvds  18709  frgpnabl  18995  ablfac1eulem  19194  ablfac1eu  19195  psgnodpm  20732  obselocv  20872  1marepvmarrepid  21184  mdetunilem9  21229  t1connperf  22044  txindislem  22241  fbasrn  22492  isufil2  22516  ufileu  22527  filufint  22528  ufilen  22538  fin1aufil  22540  alexsubALTlem4  22658  ptcmplem2  22661  itg2gt0  24361  cosord  25116  argimgt0  25195  logdivlt  25204  logrec  25341  dcubic  25424  wilthlem2  25646  bposlem3  25862  dchrisum0fno1  26087  numedglnl  26929  nbumgr  27129  uhgrnbgr0nb  27136  cusgrfi  27240  vtxduhgr0nedg  27274  uhgrvd00  27316  wlkp1lem6  27460  2wspmdisj  28116  chnlen0  29221  staddi  30023  stadd3i  30025  strlem1  30027  atoml2i  30160  prmdvdsbc  30532  psgnfzto1stlem  30742  madjusmdetlem1  31092  madjusmdetlem2  31093  hasheuni  31344  sitgaddlemb  31606  eulerpartlemb  31626  ballotlemfc0  31750  ballotlemfcc  31751  acycgrislfgr  32399  umgracycusgr  32401  acycgrsubgr  32405  funeldmb  33006  dfon2lem6  33033  exnel  33047  frpomin  33078  sltres  33169  nosepssdm  33190  nosupbnd1lem1  33208  sletr  33237  nn0prpwlem  33670  waj-ax  33762  bj-dtru  34139  sucneqond  34649  wl-spae  34776  wl-ax11-lem3  34834  lindsadd  34900  matunitlindflem1  34903  poimirlem26  34933  poimirlem28  34935  poimirlem31  34938  areacirc  35002  pridlc3  35366  lkreqN  36321  atlrelat1  36472  2llnneN  36560  cdlemg4c  37763  mapdh8e  38935  sn-dtru  39160  vk15.4j  40911  isosctrlem1ALT  41317  afvres  43420  otiunsndisjX  43527  fmtnoinf  43747  requad2  43837  copisnmnd  44125  dig1  44717  rrxsphere  44784