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  1864  nelcon3d  3065  spcimegf  3514  spcimedv  3549  rspcimedv  3567  ssneld  3910  sscon  4079  difrab  4263  disjord  5091  disjiund  5093  dtruALT2  5331  exneq  5403  otiunsndisj  5492  wereu2  5647  frpomin  6343  ndmfv  6917  dff3  7100  soisores  7335  funeldmb  7369  releldmdifi  8056  funeldmdif  8059  ressuppssdif  8203  tz7.49  8456  oaord  8556  oalimcl  8569  omord2  8576  omcan  8578  omeulem1  8591  oeord  8598  oecan  8599  nnaord  8629  nnmord  8642  nneob  8666  omsmo  8668  domtriord  9143  pssnn  9185  isinf  9257  frfi  9277  fisupg  9280  difinf  9304  supmo  9445  infmo  9490  alephord  10155  fin17  10473  isfin7-2  10475  fin1a2lem12  10490  fpwwe2lem12  10728  prub  11080  genpnnp  11091  ltaddpr  11120  prlem936  11133  ltadd2  11415  ltord1  11843  ltmul1  12168  lt2msq  12203  nnge1  12367  nzadd  12745  zeo  12786  irradd  13102  irrmul  13103  mul2lt0bi  13229  supxrun  13447  supxrgtmnf  13460  ssfzoulel  13896  zesq  14371  bccmpl  14454  fundmge2nop0  14648  repswswrd  14936  s3iunsndisj  15122  lcmftp  16812  prm2orodd  16867  coprm  16888  prmndvdsfaclt  16902  prmdvdsbc  16903  hashgcdeq  16968  prmreclem3  17097  vdwnnlem2  17175  latnlej2  18634  mgm2nsgrplem3  19120  f1omvdco2  19663  oddvds  19762  gexdvds  19799  frgpnabl  20090  ablfac1eulem  20289  ablfac1eu  20290  cmprmidlmcl  21632  psgnodpm  21895  obselocv  22035  1marepvmarrepid  22891  mdetunilem9  22936  matunitlindflem1  22995  t1connperf  23755  txindislem  23953  fbasrn  24204  isufil2  24228  ufileu  24239  filufint  24240  ufilen  24250  fin1aufil  24252  alexsubALTlem4  24370  ptcmplem2  24373  itg2gt0  26082  cosord  26860  argimgt0  26941  logdivlt  26950  logrec  27092  dcubic  27175  wilthlem2  27397  bposlem3  27614  dchrisum0fno1  27839  ltsres  28020  nosepssdm  28044  nosupbnd1lem1  28066  lestr  28120  om2noseqf1o  28688  numedglnl  29723  nbumgr  29929  uhgrnbgr0nb  29936  cusgrfi  30040  vtxduhgr0nedg  30074  uhgrvd00  30116  wlkp1lem6  30258  2wspmdisj  30939  chnlen0  32047  staddi  32849  stadd3i  32851  strlem1  32853  atoml2i  32986  n0nsnel  33154  psgnfzto1stlem  33704  madjusmdetlem1  34502  hasheuni  34760  sitgaddlemb  35023  eulerpartlemb  35043  ballotlemfc0  35168  ballotlemfcc  35169  cbvex1v  35747  onvf1odlem4  35946  onprcf1acwevdlem1  35957  acycgrislfgr  35986  umgracycusgr  35988  acycgrsubgr  35992  dfon2lem6  36625  exnel  36639  nn0prpwlem  37185  waj-ax  37277  dfttc4lem2  37392  sucneqond  38364  wl-spae  38529  lindsadd  38612  poimirlem26  38640  poimirlem28  38642  poimirlem31  38645  areacirc  38707  pridlc3  39083  lkreqN  40303  atlrelat1  40454  2llnneN  40542  cdlemg4c  41745  mapdh8e  42917  aks4d1p7  43209  aks4d1p8  43213  primrootlekpowne0  43231  aks6d1c2p2  43245  sticksstones1  43272  mulgt0con1dlem  43609  naddwordnexlem4  44479  vk15.4j  45587  isosctrlem1ALT  45992  n0nsn2el  48171  afvres  48318  otiunsndisjX  48425  fmtnoinf  48697  requad2  48797  cycldlenngric  49102  copisnmnd  49342  dig1  49796  rrxsphere  49936