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  3065  spcimegf  3514  spcimedv  3549  rspcimedv  3567  ssneld  3932  sscon  4089  difrab  4263  disjord  5091  disjiund  5093  dtruALT2  5331  exneq  5403  otiunsndisj  5489  wereu2  5644  frpomin  6332  ndmfv  6905  dff3  7088  soisores  7323  funeldmb  7357  releldmdifi  8039  funeldmdif  8042  ressuppssdif  8180  tz7.49  8433  oaord  8533  oalimcl  8546  omord2  8553  omcan  8555  omeulem1  8568  oeord  8575  oecan  8576  nnaord  8606  nnmord  8619  nneob  8643  omsmo  8645  domtriord  9120  pssnn  9162  isinf  9234  frfi  9254  fisupg  9257  difinf  9281  supmo  9422  infmo  9467  alephord  10126  fin17  10444  isfin7-2  10446  fin1a2lem12  10461  fpwwe2lem12  10699  prub  11051  genpnnp  11062  ltaddpr  11091  prlem936  11104  ltadd2  11386  ltord1  11812  ltmul1  12137  lt2msq  12172  nnge1  12336  nzadd  12714  zeo  12755  irradd  13071  irrmul  13072  mul2lt0bi  13198  supxrun  13416  supxrgtmnf  13429  ssfzoulel  13864  zesq  14338  bccmpl  14421  fundmge2nop0  14615  repswswrd  14903  s3iunsndisj  15089  lcmftp  16774  prm2orodd  16829  coprm  16850  prmndvdsfaclt  16864  prmdvdsbc  16865  hashgcdeq  16929  prmreclem3  17058  vdwnnlem2  17136  latnlej2  18595  mgm2nsgrplem3  19081  f1omvdco2  19624  oddvds  19723  gexdvds  19760  frgpnabl  20051  ablfac1eulem  20250  ablfac1eu  20251  cmprmidlmcl  21593  psgnodpm  21856  obselocv  21996  1marepvmarrepid  22852  mdetunilem9  22897  matunitlindflem1  22956  t1connperf  23716  txindislem  23914  fbasrn  24165  isufil2  24189  ufileu  24200  filufint  24201  ufilen  24211  fin1aufil  24213  alexsubALTlem4  24331  ptcmplem2  24334  itg2gt0  26043  cosord  26823  argimgt0  26904  logdivlt  26913  logrec  27055  dcubic  27138  wilthlem2  27360  bposlem3  27577  dchrisum0fno1  27802  ltsres  27953  nosepssdm  27977  nosupbnd1lem1  27999  lestr  28053  om2noseqf1o  28621  numedglnl  29656  nbumgr  29862  uhgrnbgr0nb  29869  cusgrfi  29973  vtxduhgr0nedg  30007  uhgrvd00  30049  wlkp1lem6  30191  2wspmdisj  30872  chnlen0  31980  staddi  32782  stadd3i  32784  strlem1  32786  atoml2i  32919  n0nsnel  33045  psgnfzto1stlem  33595  madjusmdetlem1  34393  hasheuni  34651  sitgaddlemb  34915  eulerpartlemb  34935  ballotlemfc0  35060  ballotlemfcc  35061  cbvex1v  35639  onvf1odlem4  35810  acycgrislfgr  35838  umgracycusgr  35840  acycgrsubgr  35844  dfon2lem6  36472  exnel  36486  nn0prpwlem  37032  waj-ax  37124  dfttc4lem2  37239  sucneqond  38208  wl-spae  38373  lindsadd  38456  poimirlem26  38484  poimirlem28  38486  poimirlem31  38489  areacirc  38551  pridlc3  38927  lkreqN  40147  atlrelat1  40298  2llnneN  40386  cdlemg4c  41589  mapdh8e  42761  aks4d1p7  43053  aks4d1p8  43057  primrootlekpowne0  43075  aks6d1c2p2  43089  sticksstones1  43116  mulgt0con1dlem  43461  nna4b4nsq  43610  naddwordnexlem4  44346  vk15.4j  45455  isosctrlem1ALT  45860  n0nsn2el  48017  afvres  48164  otiunsndisjX  48271  fmtnoinf  48543  requad2  48643  cycldlenngric  48948  copisnmnd  49188  dig1  49642  rrxsphere  49782