Theorem con3d 152

Description: A contraposition deduction. Deduction form of con3 153. (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 130	. . 3 ⊢ (¬ ¬ 𝜓 → 𝜓)
2		con3d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 34	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝜒))
4	3	con1d 145	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  153  con3rr3  155  nsyld  156  nsyli  157  jcn  162  pm5.21ndd  380  bija  381  con3dimp  408  orim12dALT  908  aleximi  1835  nelcon3d  3060  rexim  3168  spcimegf  3519  spcimedv  3524  rspcimedv  3542  ssneld  3919  sscon  4069  difrab  4239  disjord  5058  disjiund  5060  dtru  5288  otiunsndisj  5428  wereu2  5577  frpomin  6228  ndmfv  6786  dff3  6958  soisores  7178  releldmdifi  7859  funeldmdif  7862  ressuppssdif  7972  wfrlem10OLD  8120  tz7.49  8246  oaord  8340  oalimcl  8353  omord2  8360  omcan  8362  omeulem1  8375  oeord  8381  oecan  8382  nnaord  8412  nnmord  8425  nneob  8446  omsmo  8448  domtriord  8859  pssnn  8913  isinf  8965  pssnnOLD  8969  frfi  8989  fisupg  8992  difinf  9014  supmo  9141  infmo  9184  alephord  9762  fin17  10081  isfin7-2  10083  fin1a2lem12  10098  fpwwe2lem12  10329  prub  10681  genpnnp  10692  ltaddpr  10721  prlem936  10734  ltadd2  11009  ltord1  11431  ltmul1  11755  lt2msq  11790  nnge1  11931  nzadd  12298  zeo  12336  irradd  12642  irrmul  12643  mul2lt0bi  12765  supxrun  12979  supxrgtmnf  12992  ssfzoulel  13409  zesq  13869  bccmpl  13951  fundmge2nop0  14134  repswswrd  14425  s3iunsndisj  14607  lcmftp  16269  prm2orodd  16324  coprm  16344  prmndvdsfaclt  16358  hashgcdeq  16418  prmreclem3  16547  vdwnnlem2  16625  latnlej2  18092  mgm2nsgrplem3  18474  f1omvdco2  18971  oddvds  19070  gexdvds  19104  frgpnabl  19391  ablfac1eulem  19590  ablfac1eu  19591  psgnodpm  20705  obselocv  20845  1marepvmarrepid  21632  mdetunilem9  21677  t1connperf  22495  txindislem  22692  fbasrn  22943  isufil2  22967  ufileu  22978  filufint  22979  ufilen  22989  fin1aufil  22991  alexsubALTlem4  23109  ptcmplem2  23112  itg2gt0  24830  cosord  25592  argimgt0  25672  logdivlt  25681  logrec  25818  dcubic  25901  wilthlem2  26123  bposlem3  26339  dchrisum0fno1  26564  numedglnl  27417  nbumgr  27617  uhgrnbgr0nb  27624  cusgrfi  27728  vtxduhgr0nedg  27762  uhgrvd00  27804  wlkp1lem6  27948  2wspmdisj  28602  chnlen0  29707  staddi  30509  stadd3i  30511  strlem1  30513  atoml2i  30646  prmdvdsbc  31032  psgnfzto1stlem  31269  madjusmdetlem1  31679  madjusmdetlem2  31680  hasheuni  31953  sitgaddlemb  32215  eulerpartlemb  32235  ballotlemfc0  32359  ballotlemfcc  32360  acycgrislfgr  33014  umgracycusgr  33016  acycgrsubgr  33020  funeldmb  33643  dfon2lem6  33670  exnel  33684  sltres  33792  nosepssdm  33816  nosupbnd1lem1  33838  sletr  33888  nn0prpwlem  34438  waj-ax  34530  bj-dtru  34926  sucneqond  35463  wl-spae  35607  wl-ax11-lem3  35665  lindsadd  35697  matunitlindflem1  35700  poimirlem26  35730  poimirlem28  35732  poimirlem31  35735  areacirc  35797  pridlc3  36158  lkreqN  37111  atlrelat1  37262  2llnneN  37350  cdlemg4c  38553  mapdh8e  39725  aks4d1p7  40019  aks4d1p8  40023  sticksstones1  40030  sn-dtru  40116  mulgt0con1dlem  40348  nna4b4nsq  40413  vk15.4j  42037  isosctrlem1ALT  42443  afvres  44551  otiunsndisjX  44658  fmtnoinf  44876  requad2  44963  copisnmnd  45251  dig1  45842  rrxsphere  45982