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  379  bija  380  con3dimp  408  orim12dALT  911  aleximi  1832  nelcon3d  3033  spcimegf  3517  spcimedv  3561  rspcimedv  3579  ssneld  3948  sscon  4106  difrab  4281  disjord  5096  disjiund  5098  dtruALT2  5325  exneq  5395  dtruOLD  5401  otiunsndisj  5480  wereu2  5635  frpomin  6313  ndmfv  6893  dff3  7072  soisores  7302  funeldmb  7334  releldmdifi  8024  funeldmdif  8027  ressuppssdif  8164  tz7.49  8413  oaord  8511  oalimcl  8524  omord2  8531  omcan  8533  omeulem1  8546  oeord  8552  oecan  8553  nnaord  8583  nnmord  8596  nneob  8620  omsmo  8622  domtriord  9087  pssnn  9132  isinf  9207  isinfOLD  9208  frfi  9232  fisupg  9235  difinf  9260  supmo  9403  infmo  9448  alephord  10028  fin17  10347  isfin7-2  10349  fin1a2lem12  10364  fpwwe2lem12  10595  prub  10947  genpnnp  10958  ltaddpr  10987  prlem936  11000  ltadd2  11278  ltord1  11704  ltmul1  12032  lt2msq  12068  nnge1  12214  nzadd  12581  zeo  12620  irradd  12932  irrmul  12933  mul2lt0bi  13059  supxrun  13276  supxrgtmnf  13289  ssfzoulel  13721  zesq  14191  bccmpl  14274  fundmge2nop0  14467  repswswrd  14749  s3iunsndisj  14934  lcmftp  16606  prm2orodd  16661  coprm  16681  prmndvdsfaclt  16695  prmdvdsbc  16696  hashgcdeq  16760  prmreclem3  16889  vdwnnlem2  16967  latnlej2  18418  mgm2nsgrplem3  18847  f1omvdco2  19378  oddvds  19477  gexdvds  19514  frgpnabl  19805  ablfac1eulem  20004  ablfac1eu  20005  psgnodpm  21497  obselocv  21637  1marepvmarrepid  22462  mdetunilem9  22507  t1connperf  23323  txindislem  23520  fbasrn  23771  isufil2  23795  ufileu  23806  filufint  23807  ufilen  23817  fin1aufil  23819  alexsubALTlem4  23937  ptcmplem2  23940  itg2gt0  25661  cosord  26440  argimgt0  26521  logdivlt  26530  logrec  26673  dcubic  26756  wilthlem2  26979  bposlem3  27197  dchrisum0fno1  27422  sltres  27574  nosepssdm  27598  nosupbnd1lem1  27620  sletr  27670  om2noseqf1o  28195  numedglnl  29071  nbumgr  29274  uhgrnbgr0nb  29281  cusgrfi  29386  vtxduhgr0nedg  29420  uhgrvd00  29462  wlkp1lem6  29606  2wspmdisj  30266  chnlen0  31373  staddi  32175  stadd3i  32177  strlem1  32179  atoml2i  32312  n0nsnel  32444  psgnfzto1stlem  33057  madjusmdetlem1  33817  hasheuni  34075  sitgaddlemb  34339  eulerpartlemb  34359  ballotlemfc0  34484  ballotlemfcc  34485  cbvex1v  35064  onvf1odlem4  35093  acycgrislfgr  35139  umgracycusgr  35141  acycgrsubgr  35145  dfon2lem6  35776  exnel  35790  nn0prpwlem  36310  waj-ax  36402  sucneqond  37353  wl-spae  37509  wl-ax11-lem3  37575  lindsadd  37607  matunitlindflem1  37610  poimirlem26  37640  poimirlem28  37642  poimirlem31  37645  areacirc  37707  pridlc3  38067  lkreqN  39163  atlrelat1  39314  2llnneN  39403  cdlemg4c  40606  mapdh8e  41778  aks4d1p7  42071  aks4d1p8  42075  primrootlekpowne0  42093  aks6d1c2p2  42107  sticksstones1  42134  mulgt0con1dlem  42457  nna4b4nsq  42648  naddwordnexlem4  43390  vk15.4j  44518  isosctrlem1ALT  44923  tworepnotupword  46884  n0nsn2el  47026  afvres  47173  otiunsndisjX  47280  fmtnoinf  47537  requad2  47624  cycldlenngric  47928  copisnmnd  48157  dig1  48597  rrxsphere  48737