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  379  bija  380  con3dimp  408  orim12dALT  912  aleximi  1834  nelcon3d  3041  spcimegf  3497  spcimedv  3538  rspcimedv  3556  ssneld  3924  sscon  4084  difrab  4259  disjord  5075  disjiund  5077  dtruALT2  5313  exneq  5389  otiunsndisj  5475  wereu2  5628  frpomin  6305  ndmfv  6873  dff3  7053  soisores  7282  funeldmb  7314  releldmdifi  7998  funeldmdif  8001  ressuppssdif  8135  tz7.49  8384  oaord  8482  oalimcl  8495  omord2  8502  omcan  8504  omeulem1  8517  oeord  8524  oecan  8525  nnaord  8555  nnmord  8568  nneob  8592  omsmo  8594  domtriord  9061  pssnn  9103  isinf  9175  frfi  9195  fisupg  9198  difinf  9221  supmo  9365  infmo  9410  alephord  9997  fin17  10316  isfin7-2  10318  fin1a2lem12  10333  fpwwe2lem12  10565  prub  10917  genpnnp  10928  ltaddpr  10957  prlem936  10970  ltadd2  11250  ltord1  11676  ltmul1  12005  lt2msq  12041  nnge1  12205  nzadd  12575  zeo  12615  irradd  12923  irrmul  12924  mul2lt0bi  13050  supxrun  13268  supxrgtmnf  13281  ssfzoulel  13715  zesq  14188  bccmpl  14271  fundmge2nop0  14464  repswswrd  14746  s3iunsndisj  14930  lcmftp  16605  prm2orodd  16660  coprm  16681  prmndvdsfaclt  16695  prmdvdsbc  16696  hashgcdeq  16760  prmreclem3  16889  vdwnnlem2  16967  latnlej2  18425  mgm2nsgrplem3  18891  f1omvdco2  19423  oddvds  19522  gexdvds  19559  frgpnabl  19850  ablfac1eulem  20049  ablfac1eu  20050  psgnodpm  21568  obselocv  21708  1marepvmarrepid  22540  mdetunilem9  22585  t1connperf  23401  txindislem  23598  fbasrn  23849  isufil2  23873  ufileu  23884  filufint  23885  ufilen  23895  fin1aufil  23897  alexsubALTlem4  24015  ptcmplem2  24018  itg2gt0  25727  cosord  26495  argimgt0  26576  logdivlt  26585  logrec  26727  dcubic  26810  wilthlem2  27032  bposlem3  27249  dchrisum0fno1  27474  ltsres  27626  nosepssdm  27650  nosupbnd1lem1  27672  lestr  27726  om2noseqf1o  28293  numedglnl  29213  nbumgr  29416  uhgrnbgr0nb  29423  cusgrfi  29527  vtxduhgr0nedg  29561  uhgrvd00  29603  wlkp1lem6  29745  2wspmdisj  30407  chnlen0  31515  staddi  32317  stadd3i  32319  strlem1  32321  atoml2i  32454  n0nsnel  32585  psgnfzto1stlem  33161  madjusmdetlem1  33971  hasheuni  34229  sitgaddlemb  34492  eulerpartlemb  34512  ballotlemfc0  34637  ballotlemfcc  34638  cbvex1v  35216  onvf1odlem4  35288  acycgrislfgr  35334  umgracycusgr  35336  acycgrsubgr  35340  dfon2lem6  35968  exnel  35982  nn0prpwlem  36504  waj-ax  36596  dfttc4lem2  36711  sucneqond  37681  wl-spae  37846  lindsadd  37934  matunitlindflem1  37937  poimirlem26  37967  poimirlem28  37969  poimirlem31  37972  areacirc  38034  pridlc3  38394  lkreqN  39616  atlrelat1  39767  2llnneN  39855  cdlemg4c  41058  mapdh8e  42230  aks4d1p7  42522  aks4d1p8  42526  primrootlekpowne0  42544  aks6d1c2p2  42558  sticksstones1  42585  mulgt0con1dlem  42914  nna4b4nsq  43093  naddwordnexlem4  43829  vk15.4j  44955  isosctrlem1ALT  45360  n0nsn2el  47467  afvres  47614  otiunsndisjX  47721  fmtnoinf  47993  requad2  48093  cycldlenngric  48398  copisnmnd  48639  dig1  49078  rrxsphere  49218