Theorem con3d 152

Description: A contraposition deduction. Deduction form of con3 153. (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 130	. . 3 ⊢ (¬ ¬ 𝜓 → 𝜓)
2		con3d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 34	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝜒))
4	3	con1d 145	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  153  con3rr3  155  nsyld  156  nsyli  157  jcn  162  pm5.21ndd  380  bija  381  con3dimp  409  orim12dALT  909  aleximi  1833  nelcon3d  3059  spcimegf  3538  spcimedv  3543  rspcimedv  3561  ssneld  3933  sscon  4084  difrab  4253  disjord  5075  disjiund  5077  dtruALT2  5308  exneq  5373  dtruOLD  5378  otiunsndisj  5453  wereu2  5605  frpomin  6266  ndmfv  6844  dff3  7016  soisores  7238  funeldmb  7270  releldmdifi  7933  funeldmdif  7936  ressuppssdif  8050  wfrlem10OLD  8198  tz7.49  8325  oaord  8428  oalimcl  8441  omord2  8448  omcan  8450  omeulem1  8463  oeord  8469  oecan  8470  nnaord  8500  nnmord  8513  nneob  8536  omsmo  8538  domtriord  8967  pssnn  9012  isinf  9104  isinfOLD  9105  pssnnOLD  9109  frfi  9132  fisupg  9135  difinf  9160  supmo  9288  infmo  9331  alephord  9911  fin17  10230  isfin7-2  10232  fin1a2lem12  10247  fpwwe2lem12  10478  prub  10830  genpnnp  10841  ltaddpr  10870  prlem936  10883  ltadd2  11159  ltord1  11581  ltmul1  11905  lt2msq  11940  nnge1  12081  nzadd  12448  zeo  12486  irradd  12793  irrmul  12794  mul2lt0bi  12916  supxrun  13130  supxrgtmnf  13143  ssfzoulel  13561  zesq  14021  bccmpl  14103  fundmge2nop0  14285  repswswrd  14576  s3iunsndisj  14758  lcmftp  16418  prm2orodd  16473  coprm  16493  prmndvdsfaclt  16507  hashgcdeq  16567  prmreclem3  16696  vdwnnlem2  16774  latnlej2  18254  mgm2nsgrplem3  18635  f1omvdco2  19132  oddvds  19231  gexdvds  19265  frgpnabl  19551  ablfac1eulem  19750  ablfac1eu  19751  psgnodpm  20876  obselocv  21018  1marepvmarrepid  21807  mdetunilem9  21852  t1connperf  22670  txindislem  22867  fbasrn  23118  isufil2  23142  ufileu  23153  filufint  23154  ufilen  23164  fin1aufil  23166  alexsubALTlem4  23284  ptcmplem2  23287  itg2gt0  25008  cosord  25770  argimgt0  25850  logdivlt  25859  logrec  25996  dcubic  26079  wilthlem2  26301  bposlem3  26517  dchrisum0fno1  26742  sltres  26893  nosepssdm  26917  numedglnl  27650  nbumgr  27850  uhgrnbgr0nb  27857  cusgrfi  27961  vtxduhgr0nedg  27995  uhgrvd00  28037  wlkp1lem6  28182  2wspmdisj  28837  chnlen0  29942  staddi  30744  stadd3i  30746  strlem1  30748  atoml2i  30881  prmdvdsbc  31265  psgnfzto1stlem  31502  madjusmdetlem1  31917  madjusmdetlem2  31918  hasheuni  32193  sitgaddlemb  32455  eulerpartlemb  32475  ballotlemfc0  32599  ballotlemfcc  32600  acycgrislfgr  33253  umgracycusgr  33255  acycgrsubgr  33259  dfon2lem6  33895  exnel  33909  nosupbnd1lem1  33985  sletr  34035  nn0prpwlem  34585  waj-ax  34677  sucneqond  35608  wl-spae  35752  wl-ax11-lem3  35810  lindsadd  35842  matunitlindflem1  35845  poimirlem26  35875  poimirlem28  35877  poimirlem31  35880  areacirc  35942  pridlc3  36303  lkreqN  37404  atlrelat1  37555  2llnneN  37644  cdlemg4c  38847  mapdh8e  40019  aks4d1p7  40312  aks4d1p8  40316  aks6d1c2p2  40321  sticksstones1  40326  mulgt0con1dlem  40643  nna4b4nsq  40713  vk15.4j  42382  isosctrlem1ALT  42788  afvres  44929  otiunsndisjX  45036  fmtnoinf  45253  requad2  45340  copisnmnd  45628  dig1  46219  rrxsphere  46359  tworepnotupword  46786