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  910  aleximi  1830  nelcon3d  3056  spcimegf  3563  spcimedv  3608  rspcimedv  3626  ssneld  4010  sscon  4166  difrab  4337  disjord  5155  disjiund  5157  dtruALT2  5388  exneq  5455  dtruOLD  5461  otiunsndisj  5539  wereu2  5697  frpomin  6372  ndmfv  6955  dff3  7134  soisores  7363  funeldmb  7395  releldmdifi  8086  funeldmdif  8089  ressuppssdif  8226  wfrlem10OLD  8374  tz7.49  8501  oaord  8603  oalimcl  8616  omord2  8623  omcan  8625  omeulem1  8638  oeord  8644  oecan  8645  nnaord  8675  nnmord  8688  nneob  8712  omsmo  8714  domtriord  9189  pssnn  9234  isinf  9323  isinfOLD  9324  frfi  9349  fisupg  9352  difinf  9377  supmo  9521  infmo  9564  alephord  10144  fin17  10463  isfin7-2  10465  fin1a2lem12  10480  fpwwe2lem12  10711  prub  11063  genpnnp  11074  ltaddpr  11103  prlem936  11116  ltadd2  11394  ltord1  11816  ltmul1  12144  lt2msq  12180  nnge1  12321  nzadd  12691  zeo  12729  irradd  13038  irrmul  13039  mul2lt0bi  13163  supxrun  13378  supxrgtmnf  13391  ssfzoulel  13810  zesq  14275  bccmpl  14358  fundmge2nop0  14551  repswswrd  14832  s3iunsndisj  15017  lcmftp  16683  prm2orodd  16738  coprm  16758  prmndvdsfaclt  16772  prmdvdsbc  16773  hashgcdeq  16836  prmreclem3  16965  vdwnnlem2  17043  latnlej2  18529  mgm2nsgrplem3  18955  f1omvdco2  19490  oddvds  19589  gexdvds  19626  frgpnabl  19917  ablfac1eulem  20116  ablfac1eu  20117  psgnodpm  21629  obselocv  21771  1marepvmarrepid  22602  mdetunilem9  22647  t1connperf  23465  txindislem  23662  fbasrn  23913  isufil2  23937  ufileu  23948  filufint  23949  ufilen  23959  fin1aufil  23961  alexsubALTlem4  24079  ptcmplem2  24082  itg2gt0  25815  cosord  26591  argimgt0  26672  logdivlt  26681  logrec  26824  dcubic  26907  wilthlem2  27130  bposlem3  27348  dchrisum0fno1  27573  sltres  27725  nosepssdm  27749  nosupbnd1lem1  27771  sletr  27821  om2noseqf1o  28325  numedglnl  29179  nbumgr  29382  uhgrnbgr0nb  29389  cusgrfi  29494  vtxduhgr0nedg  29528  uhgrvd00  29570  wlkp1lem6  29714  2wspmdisj  30369  chnlen0  31476  staddi  32278  stadd3i  32280  strlem1  32282  atoml2i  32415  n0nsnel  32544  psgnfzto1stlem  33093  madjusmdetlem1  33773  madjusmdetlem2  33774  hasheuni  34049  sitgaddlemb  34313  eulerpartlemb  34333  ballotlemfc0  34457  ballotlemfcc  34458  cbvex1v  35050  acycgrislfgr  35120  umgracycusgr  35122  acycgrsubgr  35126  dfon2lem6  35752  exnel  35766  nn0prpwlem  36288  waj-ax  36380  sucneqond  37331  wl-spae  37475  wl-ax11-lem3  37541  lindsadd  37573  matunitlindflem1  37576  poimirlem26  37606  poimirlem28  37608  poimirlem31  37611  areacirc  37673  pridlc3  38033  lkreqN  39126  atlrelat1  39277  2llnneN  39366  cdlemg4c  40569  mapdh8e  41741  aks4d1p7  42040  aks4d1p8  42044  primrootlekpowne0  42062  aks6d1c2p2  42076  sticksstones1  42103  mulgt0con1dlem  42433  nna4b4nsq  42615  naddwordnexlem4  43363  vk15.4j  44499  isosctrlem1ALT  44905  tworepnotupword  46805  n0nsn2el  46940  afvres  47087  otiunsndisjX  47194  fmtnoinf  47410  requad2  47497  copisnmnd  47892  dig1  48342  rrxsphere  48482