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  409  orim12dALT  917  aleximi  1839  nelcon3d  3043  spcimegf  3499  spcimedv  3540  rspcimedv  3558  ssneld  3924  sscon  4080  difrab  4253  disjord  5068  disjiund  5070  dtruALT2  5306  exneq  5382  otiunsndisj  5468  wereu2  5622  frpomin  6298  ndmfv  6866  dff3  7048  soisores  7278  funeldmb  7310  releldmdifi  7994  funeldmdif  7997  ressuppssdif  8132  tz7.49  8381  oaord  8479  oalimcl  8492  omord2  8499  omcan  8501  omeulem1  8514  oeord  8521  oecan  8522  nnaord  8552  nnmord  8565  nneob  8589  omsmo  8591  domtriord  9058  pssnn  9100  isinf  9172  frfi  9192  fisupg  9195  difinf  9218  supmo  9362  infmo  9407  alephord  9995  fin17  10314  isfin7-2  10316  fin1a2lem12  10331  fpwwe2lem12  10563  prub  10915  genpnnp  10926  ltaddpr  10955  prlem936  10968  ltadd2  11248  ltord1  11674  ltmul1  12003  lt2msq  12039  nnge1  12203  nzadd  12573  zeo  12613  irradd  12921  irrmul  12922  mul2lt0bi  13048  supxrun  13266  supxrgtmnf  13279  ssfzoulel  13713  zesq  14186  bccmpl  14269  fundmge2nop0  14462  repswswrd  14744  s3iunsndisj  14928  lcmftp  16603  prm2orodd  16658  coprm  16679  prmndvdsfaclt  16693  prmdvdsbc  16694  hashgcdeq  16758  prmreclem3  16887  vdwnnlem2  16965  latnlej2  18423  mgm2nsgrplem3  18889  f1omvdco2  19421  oddvds  19520  gexdvds  19557  frgpnabl  19848  ablfac1eulem  20047  ablfac1eu  20048  psgnodpm  21570  obselocv  21710  1marepvmarrepid  22565  mdetunilem9  22610  t1connperf  23426  txindislem  23623  fbasrn  23874  isufil2  23898  ufileu  23909  filufint  23910  ufilen  23920  fin1aufil  23922  alexsubALTlem4  24040  ptcmplem2  24043  itg2gt0  25752  cosord  26520  argimgt0  26601  logdivlt  26610  logrec  26752  dcubic  26835  wilthlem2  27057  bposlem3  27274  dchrisum0fno1  27499  ltsres  27651  nosepssdm  27675  nosupbnd1lem1  27697  lestr  27751  om2noseqf1o  28318  numedglnl  29238  nbumgr  29441  uhgrnbgr0nb  29448  cusgrfi  29552  vtxduhgr0nedg  29586  uhgrvd00  29628  wlkp1lem6  29770  2wspmdisj  30432  chnlen0  31540  staddi  32342  stadd3i  32344  strlem1  32346  atoml2i  32479  n0nsnel  32610  psgnfzto1stlem  33188  madjusmdetlem1  34018  hasheuni  34276  sitgaddlemb  34539  eulerpartlemb  34559  ballotlemfc0  34684  ballotlemfcc  34685  cbvex1v  35263  onvf1odlem4  35335  acycgrislfgr  35381  umgracycusgr  35383  acycgrsubgr  35387  dfon2lem6  36015  exnel  36029  nn0prpwlem  36551  waj-ax  36643  dfttc4lem2  36758  sucneqond  37728  wl-spae  37893  lindsadd  37981  matunitlindflem1  37984  poimirlem26  38014  poimirlem28  38016  poimirlem31  38019  areacirc  38081  pridlc3  38441  lkreqN  39663  atlrelat1  39814  2llnneN  39902  cdlemg4c  41105  mapdh8e  42277  aks4d1p7  42569  aks4d1p8  42573  primrootlekpowne0  42591  aks6d1c2p2  42605  sticksstones1  42632  mulgt0con1dlem  42960  nna4b4nsq  43111  naddwordnexlem4  43847  vk15.4j  44973  isosctrlem1ALT  45378  n0nsn2el  47489  afvres  47636  otiunsndisjX  47743  fmtnoinf  48015  requad2  48115  cycldlenngric  48420  copisnmnd  48661  dig1  49100  rrxsphere  49240