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  413  orim12dALT  924  aleximi  1861  nelcon3d  3067  spcimegf  3518  spcimedv  3553  rspcimedv  3571  ssneld  3938  sscon  4096  difrab  4270  disjord  5097  disjiund  5099  dtruALT2  5340  exneq  5416  otiunsndisj  5502  wereu2  5657  frpomin  6341  ndmfv  6913  dff3  7095  soisores  7325  funeldmb  7359  releldmdifi  8040  funeldmdif  8043  ressuppssdif  8179  tz7.49  8430  oaord  8530  oalimcl  8543  omord2  8550  omcan  8552  omeulem1  8565  oeord  8572  oecan  8573  nnaord  8603  nnmord  8616  nneob  8640  omsmo  8642  domtriord  9109  pssnn  9151  isinf  9223  frfi  9243  fisupg  9246  difinf  9269  supmo  9410  infmo  9455  alephord  10066  fin17  10384  isfin7-2  10386  fin1a2lem12  10401  fpwwe2lem12  10633  prub  10985  genpnnp  10996  ltaddpr  11025  prlem936  11038  ltadd2  11320  ltord1  11746  ltmul1  12071  lt2msq  12106  nnge1  12270  nzadd  12648  zeo  12688  irradd  13003  irrmul  13004  mul2lt0bi  13130  supxrun  13348  supxrgtmnf  13361  ssfzoulel  13796  zesq  14269  bccmpl  14352  fundmge2nop0  14546  repswswrd  14828  s3iunsndisj  15012  lcmftp  16700  prm2orodd  16755  coprm  16776  prmndvdsfaclt  16790  prmdvdsbc  16791  hashgcdeq  16855  prmreclem3  16984  vdwnnlem2  17062  latnlej2  18521  mgm2nsgrplem3  18988  f1omvdco2  19524  oddvds  19623  gexdvds  19660  frgpnabl  19951  ablfac1eulem  20150  ablfac1eu  20151  cmprmidlmcl  21486  psgnodpm  21749  obselocv  21889  1marepvmarrepid  22743  mdetunilem9  22788  t1connperf  23604  txindislem  23801  fbasrn  24052  isufil2  24076  ufileu  24087  filufint  24088  ufilen  24098  fin1aufil  24100  alexsubALTlem4  24218  ptcmplem2  24221  itg2gt0  25930  cosord  26707  argimgt0  26788  logdivlt  26797  logrec  26939  dcubic  27022  wilthlem2  27244  bposlem3  27461  dchrisum0fno1  27686  ltsres  27837  nosepssdm  27861  nosupbnd1lem1  27883  lestr  27937  om2noseqf1o  28505  numedglnl  29505  nbumgr  29708  uhgrnbgr0nb  29715  cusgrfi  29819  vtxduhgr0nedg  29853  uhgrvd00  29895  wlkp1lem6  30037  2wspmdisj  30699  chnlen0  31807  staddi  32609  stadd3i  32611  strlem1  32613  atoml2i  32746  n0nsnel  32872  psgnfzto1stlem  33429  madjusmdetlem1  34226  hasheuni  34484  sitgaddlemb  34747  eulerpartlemb  34767  ballotlemfc0  34892  ballotlemfcc  34893  cbvex1v  35471  onvf1odlem4  35598  acycgrislfgr  35652  umgracycusgr  35654  acycgrsubgr  35658  dfon2lem6  36286  exnel  36300  nn0prpwlem  36861  waj-ax  36953  dfttc4lem2  37068  sucneqond  38039  wl-spae  38204  lindsadd  38292  matunitlindflem1  38295  poimirlem26  38325  poimirlem28  38327  poimirlem31  38330  areacirc  38392  pridlc3  38752  lkreqN  39972  atlrelat1  40123  2llnneN  40211  cdlemg4c  41414  mapdh8e  42586  aks4d1p7  42878  aks4d1p8  42882  primrootlekpowne0  42900  aks6d1c2p2  42914  sticksstones1  42941  mulgt0con1dlem  43271  nna4b4nsq  43420  naddwordnexlem4  44156  vk15.4j  45265  isosctrlem1ALT  45670  n0nsn2el  47790  afvres  47937  otiunsndisjX  48044  fmtnoinf  48316  requad2  48416  cycldlenngric  48721  copisnmnd  48962  dig1  49416  rrxsphere  49556