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  910  aleximi  1834  nelcon3d  3049  spcimegf  3550  spcimedv  3555  rspcimedv  3573  ssneld  3949  sscon  4103  difrab  4273  disjord  5098  disjiund  5100  dtruALT2  5330  exneq  5397  dtruOLD  5403  otiunsndisj  5482  wereu2  5635  frpomin  6299  ndmfv  6882  dff3  7055  soisores  7277  funeldmb  7309  releldmdifi  7982  funeldmdif  7985  ressuppssdif  8121  wfrlem10OLD  8269  tz7.49  8396  oaord  8499  oalimcl  8512  omord2  8519  omcan  8521  omeulem1  8534  oeord  8540  oecan  8541  nnaord  8571  nnmord  8584  nneob  8607  omsmo  8609  domtriord  9074  pssnn  9119  isinf  9211  isinfOLD  9212  pssnnOLD  9216  frfi  9239  fisupg  9242  difinf  9267  supmo  9397  infmo  9440  alephord  10020  fin17  10339  isfin7-2  10341  fin1a2lem12  10356  fpwwe2lem12  10587  prub  10939  genpnnp  10950  ltaddpr  10979  prlem936  10992  ltadd2  11268  ltord1  11690  ltmul1  12014  lt2msq  12049  nnge1  12190  nzadd  12560  zeo  12598  irradd  12907  irrmul  12908  mul2lt0bi  13030  supxrun  13245  supxrgtmnf  13258  ssfzoulel  13676  zesq  14139  bccmpl  14219  fundmge2nop0  14403  repswswrd  14684  s3iunsndisj  14865  lcmftp  16523  prm2orodd  16578  coprm  16598  prmndvdsfaclt  16612  hashgcdeq  16672  prmreclem3  16801  vdwnnlem2  16879  latnlej2  18362  mgm2nsgrplem3  18744  f1omvdco2  19244  oddvds  19343  gexdvds  19380  frgpnabl  19667  ablfac1eulem  19865  ablfac1eu  19866  psgnodpm  21029  obselocv  21171  1marepvmarrepid  21961  mdetunilem9  22006  t1connperf  22824  txindislem  23021  fbasrn  23272  isufil2  23296  ufileu  23307  filufint  23308  ufilen  23318  fin1aufil  23320  alexsubALTlem4  23438  ptcmplem2  23441  itg2gt0  25162  cosord  25924  argimgt0  26004  logdivlt  26013  logrec  26150  dcubic  26233  wilthlem2  26455  bposlem3  26671  dchrisum0fno1  26896  sltres  27047  nosepssdm  27071  nosupbnd1lem1  27093  sletr  27143  numedglnl  28158  nbumgr  28358  uhgrnbgr0nb  28365  cusgrfi  28469  vtxduhgr0nedg  28503  uhgrvd00  28545  wlkp1lem6  28689  2wspmdisj  29344  chnlen0  30449  staddi  31251  stadd3i  31253  strlem1  31255  atoml2i  31388  prmdvdsbc  31782  psgnfzto1stlem  32019  madjusmdetlem1  32497  madjusmdetlem2  32498  hasheuni  32773  sitgaddlemb  33037  eulerpartlemb  33057  ballotlemfc0  33181  ballotlemfcc  33182  acycgrislfgr  33833  umgracycusgr  33835  acycgrsubgr  33839  dfon2lem6  34449  exnel  34463  nn0prpwlem  34870  waj-ax  34962  sucneqond  35909  wl-spae  36053  wl-ax11-lem3  36112  lindsadd  36144  matunitlindflem1  36147  poimirlem26  36177  poimirlem28  36179  poimirlem31  36182  areacirc  36244  pridlc3  36605  lkreqN  37705  atlrelat1  37856  2llnneN  37945  cdlemg4c  39148  mapdh8e  40320  aks4d1p7  40613  aks4d1p8  40617  aks6d1c2p2  40622  sticksstones1  40627  mulgt0con1dlem  40984  nna4b4nsq  41056  naddwordnexlem4  41795  vk15.4j  42932  isosctrlem1ALT  43338  tworepnotupword  45245  afvres  45524  otiunsndisjX  45631  fmtnoinf  45848  requad2  45935  copisnmnd  46223  dig1  46814  rrxsphere  46954