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  3508  spcimedv  3552  rspcimedv  3570  ssneld  3939  sscon  4096  difrab  4271  disjord  5084  disjiund  5086  dtruALT2  5312  exneq  5382  dtruOLD  5388  otiunsndisj  5467  wereu2  5620  frpomin  6292  ndmfv  6859  dff3  7038  soisores  7268  funeldmb  7300  releldmdifi  7987  funeldmdif  7990  ressuppssdif  8125  tz7.49  8374  oaord  8472  oalimcl  8485  omord2  8492  omcan  8494  omeulem1  8507  oeord  8513  oecan  8514  nnaord  8544  nnmord  8557  nneob  8581  omsmo  8583  domtriord  9047  pssnn  9092  isinf  9165  isinfOLD  9166  frfi  9190  fisupg  9193  difinf  9218  supmo  9361  infmo  9406  alephord  9988  fin17  10307  isfin7-2  10309  fin1a2lem12  10324  fpwwe2lem12  10555  prub  10907  genpnnp  10918  ltaddpr  10947  prlem936  10960  ltadd2  11238  ltord1  11664  ltmul1  11992  lt2msq  12028  nnge1  12174  nzadd  12541  zeo  12580  irradd  12892  irrmul  12893  mul2lt0bi  13019  supxrun  13236  supxrgtmnf  13249  ssfzoulel  13681  zesq  14151  bccmpl  14234  fundmge2nop0  14427  repswswrd  14708  s3iunsndisj  14893  lcmftp  16565  prm2orodd  16620  coprm  16640  prmndvdsfaclt  16654  prmdvdsbc  16655  hashgcdeq  16719  prmreclem3  16848  vdwnnlem2  16926  latnlej2  18383  mgm2nsgrplem3  18812  f1omvdco2  19345  oddvds  19444  gexdvds  19481  frgpnabl  19772  ablfac1eulem  19971  ablfac1eu  19972  psgnodpm  21513  obselocv  21653  1marepvmarrepid  22478  mdetunilem9  22523  t1connperf  23339  txindislem  23536  fbasrn  23787  isufil2  23811  ufileu  23822  filufint  23823  ufilen  23833  fin1aufil  23835  alexsubALTlem4  23953  ptcmplem2  23956  itg2gt0  25677  cosord  26456  argimgt0  26537  logdivlt  26546  logrec  26689  dcubic  26772  wilthlem2  26995  bposlem3  27213  dchrisum0fno1  27438  sltres  27590  nosepssdm  27614  nosupbnd1lem1  27636  sletr  27686  om2noseqf1o  28218  numedglnl  29107  nbumgr  29310  uhgrnbgr0nb  29317  cusgrfi  29422  vtxduhgr0nedg  29456  uhgrvd00  29498  wlkp1lem6  29640  2wspmdisj  30299  chnlen0  31406  staddi  32208  stadd3i  32210  strlem1  32212  atoml2i  32345  n0nsnel  32477  psgnfzto1stlem  33055  madjusmdetlem1  33793  hasheuni  34051  sitgaddlemb  34315  eulerpartlemb  34335  ballotlemfc0  34460  ballotlemfcc  34461  cbvex1v  35040  onvf1odlem4  35078  acycgrislfgr  35124  umgracycusgr  35126  acycgrsubgr  35130  dfon2lem6  35761  exnel  35775  nn0prpwlem  36295  waj-ax  36387  sucneqond  37338  wl-spae  37494  wl-ax11-lem3  37560  lindsadd  37592  matunitlindflem1  37595  poimirlem26  37625  poimirlem28  37627  poimirlem31  37630  areacirc  37692  pridlc3  38052  lkreqN  39148  atlrelat1  39299  2llnneN  39388  cdlemg4c  40591  mapdh8e  41763  aks4d1p7  42056  aks4d1p8  42060  primrootlekpowne0  42078  aks6d1c2p2  42092  sticksstones1  42119  mulgt0con1dlem  42442  nna4b4nsq  42633  naddwordnexlem4  43374  vk15.4j  44502  isosctrlem1ALT  44907  tworepnotupword  46868  n0nsn2el  47010  afvres  47157  otiunsndisjX  47264  fmtnoinf  47521  requad2  47608  cycldlenngric  47912  copisnmnd  48141  dig1  48581  rrxsphere  48721