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  3040  spcimegf  3530  spcimedv  3574  rspcimedv  3592  ssneld  3960  sscon  4118  difrab  4293  disjord  5108  disjiund  5110  dtruALT2  5340  exneq  5410  dtruOLD  5416  otiunsndisj  5495  wereu2  5651  frpomin  6329  ndmfv  6911  dff3  7090  soisores  7320  funeldmb  7352  releldmdifi  8044  funeldmdif  8047  ressuppssdif  8184  wfrlem10OLD  8332  tz7.49  8459  oaord  8559  oalimcl  8572  omord2  8579  omcan  8581  omeulem1  8594  oeord  8600  oecan  8601  nnaord  8631  nnmord  8644  nneob  8668  omsmo  8670  domtriord  9137  pssnn  9182  isinf  9268  isinfOLD  9269  frfi  9293  fisupg  9296  difinf  9321  supmo  9464  infmo  9509  alephord  10089  fin17  10408  isfin7-2  10410  fin1a2lem12  10425  fpwwe2lem12  10656  prub  11008  genpnnp  11019  ltaddpr  11048  prlem936  11061  ltadd2  11339  ltord1  11763  ltmul1  12091  lt2msq  12127  nnge1  12268  nzadd  12640  zeo  12679  irradd  12989  irrmul  12990  mul2lt0bi  13115  supxrun  13332  supxrgtmnf  13345  ssfzoulel  13776  zesq  14244  bccmpl  14327  fundmge2nop0  14520  repswswrd  14802  s3iunsndisj  14987  lcmftp  16655  prm2orodd  16710  coprm  16730  prmndvdsfaclt  16744  prmdvdsbc  16745  hashgcdeq  16809  prmreclem3  16938  vdwnnlem2  17016  latnlej2  18469  mgm2nsgrplem3  18898  f1omvdco2  19429  oddvds  19528  gexdvds  19565  frgpnabl  19856  ablfac1eulem  20055  ablfac1eu  20056  psgnodpm  21548  obselocv  21688  1marepvmarrepid  22513  mdetunilem9  22558  t1connperf  23374  txindislem  23571  fbasrn  23822  isufil2  23846  ufileu  23857  filufint  23858  ufilen  23868  fin1aufil  23870  alexsubALTlem4  23988  ptcmplem2  23991  itg2gt0  25713  cosord  26492  argimgt0  26573  logdivlt  26582  logrec  26725  dcubic  26808  wilthlem2  27031  bposlem3  27249  dchrisum0fno1  27474  sltres  27626  nosepssdm  27650  nosupbnd1lem1  27672  sletr  27722  om2noseqf1o  28247  numedglnl  29123  nbumgr  29326  uhgrnbgr0nb  29333  cusgrfi  29438  vtxduhgr0nedg  29472  uhgrvd00  29514  wlkp1lem6  29658  2wspmdisj  30318  chnlen0  31425  staddi  32227  stadd3i  32229  strlem1  32231  atoml2i  32364  n0nsnel  32496  psgnfzto1stlem  33111  madjusmdetlem1  33858  hasheuni  34116  sitgaddlemb  34380  eulerpartlemb  34400  ballotlemfc0  34525  ballotlemfcc  34526  cbvex1v  35105  acycgrislfgr  35174  umgracycusgr  35176  acycgrsubgr  35180  dfon2lem6  35806  exnel  35820  nn0prpwlem  36340  waj-ax  36432  sucneqond  37383  wl-spae  37539  wl-ax11-lem3  37605  lindsadd  37637  matunitlindflem1  37640  poimirlem26  37670  poimirlem28  37672  poimirlem31  37675  areacirc  37737  pridlc3  38097  lkreqN  39188  atlrelat1  39339  2llnneN  39428  cdlemg4c  40631  mapdh8e  41803  aks4d1p7  42096  aks4d1p8  42100  primrootlekpowne0  42118  aks6d1c2p2  42132  sticksstones1  42159  mulgt0con1dlem  42500  nna4b4nsq  42683  naddwordnexlem4  43425  vk15.4j  44553  isosctrlem1ALT  44958  tworepnotupword  46915  n0nsn2el  47054  afvres  47201  otiunsndisjX  47308  fmtnoinf  47550  requad2  47637  cycldlenngric  47941  copisnmnd  48144  dig1  48588  rrxsphere  48728