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  381  bija  382  con3dimp  411  orim12dALT  920  aleximi  1846  nelcon3d  3059  spcimegf  3513  spcimedv  3549  rspcimedv  3567  ssneld  3933  sscon  4091  difrab  4265  disjord  5083  disjiund  5085  dtruALT2  5321  exneq  5397  otiunsndisj  5483  wereu2  5637  frpomin  6316  ndmfv  6888  dff3  7070  soisores  7300  funeldmb  7332  releldmdifi  8015  funeldmdif  8018  ressuppssdif  8153  tz7.49  8404  oaord  8504  oalimcl  8517  omord2  8524  omcan  8526  omeulem1  8539  oeord  8546  oecan  8547  nnaord  8577  nnmord  8590  nneob  8614  omsmo  8616  domtriord  9084  pssnn  9126  isinf  9198  frfi  9218  fisupg  9221  difinf  9244  supmo  9388  infmo  9433  alephord  10021  fin17  10341  isfin7-2  10343  fin1a2lem12  10358  fpwwe2lem12  10590  prub  10942  genpnnp  10953  ltaddpr  10982  prlem936  10995  ltadd2  11277  ltord1  11703  ltmul1  12031  lt2msq  12067  nnge1  12231  nzadd  12609  zeo  12649  irradd  12964  irrmul  12965  mul2lt0bi  13091  supxrun  13309  supxrgtmnf  13322  ssfzoulel  13756  zesq  14229  bccmpl  14312  fundmge2nop0  14505  repswswrd  14787  s3iunsndisj  14971  lcmftp  16646  prm2orodd  16701  coprm  16722  prmndvdsfaclt  16736  prmdvdsbc  16737  hashgcdeq  16801  prmreclem3  16930  vdwnnlem2  17008  latnlej2  18467  mgm2nsgrplem3  18933  f1omvdco2  19464  oddvds  19563  gexdvds  19600  frgpnabl  19891  ablfac1eulem  20090  ablfac1eu  20091  psgnodpm  21613  obselocv  21753  1marepvmarrepid  22608  mdetunilem9  22653  t1connperf  23469  txindislem  23666  fbasrn  23917  isufil2  23941  ufileu  23952  filufint  23953  ufilen  23963  fin1aufil  23965  alexsubALTlem4  24083  ptcmplem2  24086  itg2gt0  25795  cosord  26566  argimgt0  26647  logdivlt  26656  logrec  26798  dcubic  26881  wilthlem2  27103  bposlem3  27320  dchrisum0fno1  27545  ltsres  27696  nosepssdm  27720  nosupbnd1lem1  27742  lestr  27796  om2noseqf1o  28364  numedglnl  29284  nbumgr  29487  uhgrnbgr0nb  29494  cusgrfi  29598  vtxduhgr0nedg  29632  uhgrvd00  29674  wlkp1lem6  29816  2wspmdisj  30478  chnlen0  31586  staddi  32388  stadd3i  32390  strlem1  32392  atoml2i  32525  n0nsnel  32656  psgnfzto1stlem  33234  madjusmdetlem1  34078  hasheuni  34336  sitgaddlemb  34599  eulerpartlemb  34619  ballotlemfc0  34744  ballotlemfcc  34745  cbvex1v  35326  onvf1odlem4  35404  acycgrislfgr  35450  umgracycusgr  35452  acycgrsubgr  35456  dfon2lem6  36084  exnel  36098  nn0prpwlem  36630  waj-ax  36722  dfttc4lem2  36837  sucneqond  37807  wl-spae  37972  lindsadd  38060  matunitlindflem1  38063  poimirlem26  38093  poimirlem28  38095  poimirlem31  38098  areacirc  38160  pridlc3  38520  lkreqN  39742  atlrelat1  39893  2llnneN  39981  cdlemg4c  41184  mapdh8e  42356  aks4d1p7  42648  aks4d1p8  42652  primrootlekpowne0  42670  aks6d1c2p2  42684  sticksstones1  42711  mulgt0con1dlem  43039  nna4b4nsq  43190  naddwordnexlem4  43926  vk15.4j  45052  isosctrlem1ALT  45457  n0nsn2el  47567  afvres  47714  otiunsndisjX  47821  fmtnoinf  48093  requad2  48193  cycldlenngric  48498  copisnmnd  48739  dig1  49178  rrxsphere  49318