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  3034  spcimegf  3520  spcimedv  3564  rspcimedv  3582  ssneld  3951  sscon  4109  difrab  4284  disjord  5099  disjiund  5101  dtruALT2  5328  exneq  5398  dtruOLD  5404  otiunsndisj  5483  wereu2  5638  frpomin  6316  ndmfv  6896  dff3  7075  soisores  7305  funeldmb  7337  releldmdifi  8027  funeldmdif  8030  ressuppssdif  8167  tz7.49  8416  oaord  8514  oalimcl  8527  omord2  8534  omcan  8536  omeulem1  8549  oeord  8555  oecan  8556  nnaord  8586  nnmord  8599  nneob  8623  omsmo  8625  domtriord  9093  pssnn  9138  isinf  9214  isinfOLD  9215  frfi  9239  fisupg  9242  difinf  9267  supmo  9410  infmo  9455  alephord  10035  fin17  10354  isfin7-2  10356  fin1a2lem12  10371  fpwwe2lem12  10602  prub  10954  genpnnp  10965  ltaddpr  10994  prlem936  11007  ltadd2  11285  ltord1  11711  ltmul1  12039  lt2msq  12075  nnge1  12221  nzadd  12588  zeo  12627  irradd  12939  irrmul  12940  mul2lt0bi  13066  supxrun  13283  supxrgtmnf  13296  ssfzoulel  13728  zesq  14198  bccmpl  14281  fundmge2nop0  14474  repswswrd  14756  s3iunsndisj  14941  lcmftp  16613  prm2orodd  16668  coprm  16688  prmndvdsfaclt  16702  prmdvdsbc  16703  hashgcdeq  16767  prmreclem3  16896  vdwnnlem2  16974  latnlej2  18425  mgm2nsgrplem3  18854  f1omvdco2  19385  oddvds  19484  gexdvds  19521  frgpnabl  19812  ablfac1eulem  20011  ablfac1eu  20012  psgnodpm  21504  obselocv  21644  1marepvmarrepid  22469  mdetunilem9  22514  t1connperf  23330  txindislem  23527  fbasrn  23778  isufil2  23802  ufileu  23813  filufint  23814  ufilen  23824  fin1aufil  23826  alexsubALTlem4  23944  ptcmplem2  23947  itg2gt0  25668  cosord  26447  argimgt0  26528  logdivlt  26537  logrec  26680  dcubic  26763  wilthlem2  26986  bposlem3  27204  dchrisum0fno1  27429  sltres  27581  nosepssdm  27605  nosupbnd1lem1  27627  sletr  27677  om2noseqf1o  28202  numedglnl  29078  nbumgr  29281  uhgrnbgr0nb  29288  cusgrfi  29393  vtxduhgr0nedg  29427  uhgrvd00  29469  wlkp1lem6  29613  2wspmdisj  30273  chnlen0  31380  staddi  32182  stadd3i  32184  strlem1  32186  atoml2i  32319  n0nsnel  32451  psgnfzto1stlem  33064  madjusmdetlem1  33824  hasheuni  34082  sitgaddlemb  34346  eulerpartlemb  34366  ballotlemfc0  34491  ballotlemfcc  34492  cbvex1v  35071  onvf1odlem4  35100  acycgrislfgr  35146  umgracycusgr  35148  acycgrsubgr  35152  dfon2lem6  35783  exnel  35797  nn0prpwlem  36317  waj-ax  36409  sucneqond  37360  wl-spae  37516  wl-ax11-lem3  37582  lindsadd  37614  matunitlindflem1  37617  poimirlem26  37647  poimirlem28  37649  poimirlem31  37652  areacirc  37714  pridlc3  38074  lkreqN  39170  atlrelat1  39321  2llnneN  39410  cdlemg4c  40613  mapdh8e  41785  aks4d1p7  42078  aks4d1p8  42082  primrootlekpowne0  42100  aks6d1c2p2  42114  sticksstones1  42141  mulgt0con1dlem  42464  nna4b4nsq  42655  naddwordnexlem4  43397  vk15.4j  44525  isosctrlem1ALT  44930  tworepnotupword  46891  n0nsn2el  47030  afvres  47177  otiunsndisjX  47284  fmtnoinf  47541  requad2  47628  cycldlenngric  47932  copisnmnd  48161  dig1  48601  rrxsphere  48741