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  1833  nelcon3d  3036  spcimegf  3504  spcimedv  3545  rspcimedv  3563  ssneld  3931  sscon  4092  difrab  4267  disjord  5082  disjiund  5084  dtruALT2  5310  exneq  5380  otiunsndisj  5463  wereu2  5616  frpomin  6293  ndmfv  6860  dff3  7039  soisores  7267  funeldmb  7299  releldmdifi  7983  funeldmdif  7986  ressuppssdif  8121  tz7.49  8370  oaord  8468  oalimcl  8481  omord2  8488  omcan  8490  omeulem1  8503  oeord  8509  oecan  8510  nnaord  8540  nnmord  8553  nneob  8577  omsmo  8579  domtriord  9042  pssnn  9084  isinf  9155  frfi  9175  fisupg  9178  difinf  9201  supmo  9342  infmo  9387  alephord  9972  fin17  10291  isfin7-2  10293  fin1a2lem12  10308  fpwwe2lem12  10539  prub  10891  genpnnp  10902  ltaddpr  10931  prlem936  10944  ltadd2  11223  ltord1  11649  ltmul1  11977  lt2msq  12013  nnge1  12159  nzadd  12526  zeo  12565  irradd  12877  irrmul  12878  mul2lt0bi  13004  supxrun  13221  supxrgtmnf  13234  ssfzoulel  13666  zesq  14139  bccmpl  14222  fundmge2nop0  14415  repswswrd  14697  s3iunsndisj  14881  lcmftp  16553  prm2orodd  16608  coprm  16628  prmndvdsfaclt  16642  prmdvdsbc  16643  hashgcdeq  16707  prmreclem3  16836  vdwnnlem2  16914  latnlej2  18371  mgm2nsgrplem3  18834  f1omvdco2  19366  oddvds  19465  gexdvds  19502  frgpnabl  19793  ablfac1eulem  19992  ablfac1eu  19993  psgnodpm  21531  obselocv  21671  1marepvmarrepid  22496  mdetunilem9  22541  t1connperf  23357  txindislem  23554  fbasrn  23805  isufil2  23829  ufileu  23840  filufint  23841  ufilen  23851  fin1aufil  23853  alexsubALTlem4  23971  ptcmplem2  23974  itg2gt0  25694  cosord  26473  argimgt0  26554  logdivlt  26563  logrec  26706  dcubic  26789  wilthlem2  27012  bposlem3  27230  dchrisum0fno1  27455  sltres  27607  nosepssdm  27631  nosupbnd1lem1  27653  sletr  27703  om2noseqf1o  28237  numedglnl  29129  nbumgr  29332  uhgrnbgr0nb  29339  cusgrfi  29444  vtxduhgr0nedg  29478  uhgrvd00  29520  wlkp1lem6  29662  2wspmdisj  30324  chnlen0  31431  staddi  32233  stadd3i  32235  strlem1  32237  atoml2i  32370  n0nsnel  32502  psgnfzto1stlem  33076  madjusmdetlem1  33847  hasheuni  34105  sitgaddlemb  34368  eulerpartlemb  34388  ballotlemfc0  34513  ballotlemfcc  34514  cbvex1v  35093  onvf1odlem4  35157  acycgrislfgr  35203  umgracycusgr  35205  acycgrsubgr  35209  dfon2lem6  35837  exnel  35851  nn0prpwlem  36373  waj-ax  36465  sucneqond  37416  wl-spae  37572  lindsadd  37659  matunitlindflem1  37662  poimirlem26  37692  poimirlem28  37694  poimirlem31  37697  areacirc  37759  pridlc3  38119  lkreqN  39275  atlrelat1  39426  2llnneN  39514  cdlemg4c  40717  mapdh8e  41889  aks4d1p7  42182  aks4d1p8  42186  primrootlekpowne0  42204  aks6d1c2p2  42218  sticksstones1  42245  mulgt0con1dlem  42568  nna4b4nsq  42759  naddwordnexlem4  43499  vk15.4j  44626  isosctrlem1ALT  45031  n0nsn2el  47130  afvres  47277  otiunsndisjX  47384  fmtnoinf  47641  requad2  47728  cycldlenngric  48033  copisnmnd  48274  dig1  48714  rrxsphere  48854