Theorem con3d 147

Description: A contraposition deduction. Deduction form of con3 148. (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 124	. . 3 ⊢ (¬ ¬ 𝜓 → 𝜓)
2		con3d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 33	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝜒))
4	3	con1d 138	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  148  con3rr3  150  nsyld  153  nsyli  154  mth8  157  pm2.52  166  pm5.21ndd  368  bija  369  con3dimp  456  aleximi  1749  nelcon3d  2895  rexim  2991  spcimegf  3260  spcimedv  3265  rspcimedv  3284  ssneld  3570  sscon  3706  difrab  3860  eqoreldifOLD  4173  dtru  4783  otiunsndisj  4905  wereu2  5035  ndmfv  6128  dff3  6280  soisores  6477  ressuppssdif  7203  wfrlem10  7311  tz7.49  7427  oaord  7514  oalimcl  7527  omord2  7534  omcan  7536  omeulem1  7549  oeord  7555  oecan  7556  nnaord  7586  nnmord  7599  nneob  7619  omsmo  7621  domtriord  7991  isinf  8058  pssnn  8063  frfi  8090  fisupg  8093  difinf  8115  supmo  8241  infmo  8284  fiinfg  8288  alephord  8781  fin17  9099  isfin7-2  9101  fin1a2lem12  9116  fpwwe2lem13  9343  prub  9695  genpnnp  9706  ltaddpr  9735  prlem936  9748  ltadd2  10020  ltord1  10433  prodge0  10749  ltmul1  10752  lt2msq  10787  nnge1  10923  nzadd  11302  zeo  11339  irradd  11688  irrmul  11689  mul2lt0bi  11812  supxrun  12018  supxrgtmnf  12031  ssfzoulel  12428  zesq  12849  bccmpl  12958  fundmge2nop0  13129  repswswrd  13382  s3iunsndisj  13555  lcmftp  15187  prm2orodd  15242  coprm  15261  prmndvdsfaclt  15273  hashgcdeq  15332  prmreclem3  15460  vdwnnlem2  15538  latnlej2  16894  mgm2nsgrplem3  17230  f1omvdco2  17691  oddvds  17789  gexdvds  17822  frgpnabl  18101  ablfac1eulem  18294  ablfac1eu  18295  psgnodpm  19753  obselocv  19891  1marepvmarrepid  20200  mdetunilem9  20245  t1conperf  21049  txindislem  21246  fbasrn  21498  isufil2  21522  ufileu  21533  filufint  21534  ufilen  21544  fin1aufil  21546  alexsubALTlem4  21664  ptcmplem2  21667  itg2gt0  23333  cosord  24082  argimgt0  24162  logdivlt  24171  logrec  24301  dcubic  24373  wilthlem2  24595  bposlem3  24811  dchrisum0fno1  25000  usgranloop0  25909  nbgra0nb  25958  nbcusgra  25992  cusgrafi  26010  vdusgra0nedg  26435  usgravd0nedg  26445  usgravd00  26446  2spotmdisj  26595  chnlen0  27687  staddi  28489  stadd3i  28491  strlem1  28493  atoml2i  28626  psgnfzto1stlem  29181  madjusmdetlem1  29221  madjusmdetlem2  29222  hasheuni  29474  sitgaddlemb  29737  eulerpartlemb  29757  ballotlemfc0  29881  ballotlemfcc  29882  dfon2lem6  30937  exnel  30952  sltres  31061  nodenselem4  31083  nofulllem5  31105  nn0prpwlem  31487  waj-ax  31583  bj-dtru  31985  sucneqond  32389  wl-spae  32485  wl-ax11-lem3  32543  matunitlindflem1  32575  poimirlem26  32605  poimirlem28  32607  poimirlem31  32610  areacirc  32675  pridlc3  33042  lkreqN  33475  atlrelat1  33626  2llnneN  33713  cdlemg4c  34918  mapdh8e  36091  vk15.4j  37755  isosctrlem1ALT  38192  afvres  39901  fmtnoinf  39986  otiunsndisjX  40317  nbumgr  40569  uhgrnbgr0nb  40576  cusgrfi  40674  vtxduhgr0nedg  40707  uhgrvd00  40750  1wlkp1lem6  40887  2wspdisj  41165  2wspmdisj  41501  copisnmnd  41599  dig1  42200