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  409  orim12dALT  909  aleximi  1835  nelcon3d  3062  spcimegf  3530  spcimedv  3535  rspcimedv  3553  ssneld  3924  sscon  4074  difrab  4243  disjord  5063  disjiund  5065  dtruALT2  5294  dtru  5360  otiunsndisj  5435  wereu2  5587  frpomin  6247  ndmfv  6813  dff3  6985  soisores  7207  releldmdifi  7895  funeldmdif  7898  ressuppssdif  8010  wfrlem10OLD  8158  tz7.49  8285  oaord  8387  oalimcl  8400  omord2  8407  omcan  8409  omeulem1  8422  oeord  8428  oecan  8429  nnaord  8459  nnmord  8472  nneob  8495  omsmo  8497  domtriord  8919  pssnn  8960  isinf  9045  pssnnOLD  9049  frfi  9068  fisupg  9071  difinf  9093  supmo  9220  infmo  9263  alephord  9840  fin17  10159  isfin7-2  10161  fin1a2lem12  10176  fpwwe2lem12  10407  prub  10759  genpnnp  10770  ltaddpr  10799  prlem936  10812  ltadd2  11088  ltord1  11510  ltmul1  11834  lt2msq  11869  nnge1  12010  nzadd  12377  zeo  12415  irradd  12722  irrmul  12723  mul2lt0bi  12845  supxrun  13059  supxrgtmnf  13072  ssfzoulel  13490  zesq  13950  bccmpl  14032  fundmge2nop0  14215  repswswrd  14506  s3iunsndisj  14688  lcmftp  16350  prm2orodd  16405  coprm  16425  prmndvdsfaclt  16439  hashgcdeq  16499  prmreclem3  16628  vdwnnlem2  16706  latnlej2  18186  mgm2nsgrplem3  18568  f1omvdco2  19065  oddvds  19164  gexdvds  19198  frgpnabl  19485  ablfac1eulem  19684  ablfac1eu  19685  psgnodpm  20802  obselocv  20944  1marepvmarrepid  21733  mdetunilem9  21778  t1connperf  22596  txindislem  22793  fbasrn  23044  isufil2  23068  ufileu  23079  filufint  23080  ufilen  23090  fin1aufil  23092  alexsubALTlem4  23210  ptcmplem2  23213  itg2gt0  24934  cosord  25696  argimgt0  25776  logdivlt  25785  logrec  25922  dcubic  26005  wilthlem2  26227  bposlem3  26443  dchrisum0fno1  26668  numedglnl  27523  nbumgr  27723  uhgrnbgr0nb  27730  cusgrfi  27834  vtxduhgr0nedg  27868  uhgrvd00  27910  wlkp1lem6  28055  2wspmdisj  28710  chnlen0  29815  staddi  30617  stadd3i  30619  strlem1  30621  atoml2i  30754  prmdvdsbc  31139  psgnfzto1stlem  31376  madjusmdetlem1  31786  madjusmdetlem2  31787  hasheuni  32062  sitgaddlemb  32324  eulerpartlemb  32344  ballotlemfc0  32468  ballotlemfcc  32469  acycgrislfgr  33123  umgracycusgr  33125  acycgrsubgr  33129  funeldmb  33746  dfon2lem6  33773  exnel  33787  sltres  33874  nosepssdm  33898  nosupbnd1lem1  33920  sletr  33970  nn0prpwlem  34520  waj-ax  34612  bj-dtru  35008  sucneqond  35545  wl-spae  35689  wl-ax11-lem3  35747  lindsadd  35779  matunitlindflem1  35782  poimirlem26  35812  poimirlem28  35814  poimirlem31  35817  areacirc  35879  pridlc3  36240  lkreqN  37191  atlrelat1  37342  2llnneN  37430  cdlemg4c  38633  mapdh8e  39805  aks4d1p7  40098  aks4d1p8  40102  sticksstones1  40109  sn-dtru  40195  mulgt0con1dlem  40434  nna4b4nsq  40504  vk15.4j  42155  isosctrlem1ALT  42561  afvres  44675  otiunsndisjX  44782  fmtnoinf  44999  requad2  45086  copisnmnd  45374  dig1  45965  rrxsphere  46105  tworepnotupword  46532