Theorem con3d 153

Description: A contraposition deduction. Deduction form of con3 154. (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 131	. . 3 ⊢ (¬ ¬ 𝜓 → 𝜓)
2		con3d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 35	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝜒))
4	3	con1d 146	1 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  con3  154  con3rr3  156  nsyld  157  nsyli  158  jcn  163  pm5.21ndd  382  bija  383  con3dimp  414  orim12dALT  925  aleximi  1865  nelcon3d  3067  spcimegf  3517  spcimedv  3552  rspcimedv  3570  ssneld  3936  sscon  4093  difrab  4267  disjord  5096  disjiund  5098  dtruALT2  5339  exneq  5415  otiunsndisj  5501  wereu2  5656  frpomin  6342  ndmfv  6914  dff3  7096  soisores  7331  funeldmb  7365  releldmdifi  8045  funeldmdif  8048  ressuppssdif  8186  tz7.49  8437  oaord  8537  oalimcl  8550  omord2  8557  omcan  8559  omeulem1  8572  oeord  8579  oecan  8580  nnaord  8610  nnmord  8623  nneob  8647  omsmo  8649  domtriord  9124  pssnn  9166  isinf  9238  frfi  9258  fisupg  9261  difinf  9284  supmo  9425  infmo  9470  alephord  10081  fin17  10399  isfin7-2  10401  fin1a2lem12  10416  fpwwe2lem12  10654  prub  11006  genpnnp  11017  ltaddpr  11046  prlem936  11059  ltadd2  11341  ltord1  11767  ltmul1  12092  lt2msq  12127  nnge1  12291  nzadd  12669  zeo  12710  irradd  13025  irrmul  13026  mul2lt0bi  13152  supxrun  13370  supxrgtmnf  13383  ssfzoulel  13818  zesq  14292  bccmpl  14375  fundmge2nop0  14569  repswswrd  14857  s3iunsndisj  15043  lcmftp  16730  prm2orodd  16785  coprm  16806  prmndvdsfaclt  16820  prmdvdsbc  16821  hashgcdeq  16885  prmreclem3  17014  vdwnnlem2  17092  latnlej2  18551  mgm2nsgrplem3  19036  f1omvdco2  19579  oddvds  19678  gexdvds  19715  frgpnabl  20006  ablfac1eulem  20205  ablfac1eu  20206  cmprmidlmcl  21542  psgnodpm  21805  obselocv  21945  1marepvmarrepid  22801  mdetunilem9  22846  matunitlindflem1  22905  t1connperf  23665  txindislem  23863  fbasrn  24114  isufil2  24138  ufileu  24149  filufint  24150  ufilen  24160  fin1aufil  24162  alexsubALTlem4  24280  ptcmplem2  24283  itg2gt0  25992  cosord  26769  argimgt0  26850  logdivlt  26859  logrec  27001  dcubic  27084  wilthlem2  27306  bposlem3  27523  dchrisum0fno1  27748  ltsres  27899  nosepssdm  27923  nosupbnd1lem1  27945  lestr  27999  om2noseqf1o  28567  numedglnl  29602  nbumgr  29808  uhgrnbgr0nb  29815  cusgrfi  29919  vtxduhgr0nedg  29953  uhgrvd00  29995  wlkp1lem6  30137  2wspmdisj  30818  chnlen0  31926  staddi  32728  stadd3i  32730  strlem1  32732  atoml2i  32865  n0nsnel  32991  psgnfzto1stlem  33542  madjusmdetlem1  34339  hasheuni  34597  sitgaddlemb  34861  eulerpartlemb  34881  ballotlemfc0  35006  ballotlemfcc  35007  cbvex1v  35585  onvf1odlem4  35705  acycgrislfgr  35733  umgracycusgr  35735  acycgrsubgr  35739  dfon2lem6  36367  exnel  36381  nn0prpwlem  36943  waj-ax  37035  dfttc4lem2  37150  sucneqond  38121  wl-spae  38286  lindsadd  38369  poimirlem26  38397  poimirlem28  38399  poimirlem31  38402  areacirc  38464  pridlc3  38825  lkreqN  40045  atlrelat1  40196  2llnneN  40284  cdlemg4c  41487  mapdh8e  42659  aks4d1p7  42951  aks4d1p8  42955  primrootlekpowne0  42973  aks6d1c2p2  42987  sticksstones1  43014  mulgt0con1dlem  43359  nna4b4nsq  43508  naddwordnexlem4  44244  vk15.4j  45353  isosctrlem1ALT  45758  n0nsn2el  47915  afvres  48062  otiunsndisjX  48169  fmtnoinf  48441  requad2  48541  cycldlenngric  48846  copisnmnd  49086  dig1  49540  rrxsphere  49680