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  1828  nelcon3d  3047  spcimegf  3550  spcimedv  3594  rspcimedv  3612  ssneld  3996  sscon  4152  difrab  4323  disjord  5136  disjiund  5138  dtruALT2  5375  exneq  5445  dtruOLD  5451  otiunsndisj  5529  wereu2  5685  frpomin  6362  ndmfv  6941  dff3  7119  soisores  7346  funeldmb  7378  releldmdifi  8068  funeldmdif  8071  ressuppssdif  8208  wfrlem10OLD  8356  tz7.49  8483  oaord  8583  oalimcl  8596  omord2  8603  omcan  8605  omeulem1  8618  oeord  8624  oecan  8625  nnaord  8655  nnmord  8668  nneob  8692  omsmo  8694  domtriord  9161  pssnn  9206  isinf  9293  isinfOLD  9294  frfi  9318  fisupg  9321  difinf  9346  supmo  9489  infmo  9532  alephord  10112  fin17  10431  isfin7-2  10433  fin1a2lem12  10448  fpwwe2lem12  10679  prub  11031  genpnnp  11042  ltaddpr  11071  prlem936  11084  ltadd2  11362  ltord1  11786  ltmul1  12114  lt2msq  12150  nnge1  12291  nzadd  12662  zeo  12701  irradd  13012  irrmul  13013  mul2lt0bi  13138  supxrun  13354  supxrgtmnf  13367  ssfzoulel  13795  zesq  14261  bccmpl  14344  fundmge2nop0  14537  repswswrd  14818  s3iunsndisj  15003  lcmftp  16669  prm2orodd  16724  coprm  16744  prmndvdsfaclt  16758  prmdvdsbc  16759  hashgcdeq  16822  prmreclem3  16951  vdwnnlem2  17029  latnlej2  18516  mgm2nsgrplem3  18945  f1omvdco2  19480  oddvds  19579  gexdvds  19616  frgpnabl  19907  ablfac1eulem  20106  ablfac1eu  20107  psgnodpm  21623  obselocv  21765  1marepvmarrepid  22596  mdetunilem9  22641  t1connperf  23459  txindislem  23656  fbasrn  23907  isufil2  23931  ufileu  23942  filufint  23943  ufilen  23953  fin1aufil  23955  alexsubALTlem4  24073  ptcmplem2  24076  itg2gt0  25809  cosord  26587  argimgt0  26668  logdivlt  26677  logrec  26820  dcubic  26903  wilthlem2  27126  bposlem3  27344  dchrisum0fno1  27569  sltres  27721  nosepssdm  27745  nosupbnd1lem1  27767  sletr  27817  om2noseqf1o  28321  numedglnl  29175  nbumgr  29378  uhgrnbgr0nb  29385  cusgrfi  29490  vtxduhgr0nedg  29524  uhgrvd00  29566  wlkp1lem6  29710  2wspmdisj  30365  chnlen0  31472  staddi  32274  stadd3i  32276  strlem1  32278  atoml2i  32411  n0nsnel  32542  psgnfzto1stlem  33102  madjusmdetlem1  33787  hasheuni  34065  sitgaddlemb  34329  eulerpartlemb  34349  ballotlemfc0  34473  ballotlemfcc  34474  cbvex1v  35066  acycgrislfgr  35136  umgracycusgr  35138  acycgrsubgr  35142  dfon2lem6  35769  exnel  35783  nn0prpwlem  36304  waj-ax  36396  sucneqond  37347  wl-spae  37501  wl-ax11-lem3  37567  lindsadd  37599  matunitlindflem1  37602  poimirlem26  37632  poimirlem28  37634  poimirlem31  37637  areacirc  37699  pridlc3  38059  lkreqN  39151  atlrelat1  39302  2llnneN  39391  cdlemg4c  40594  mapdh8e  41766  aks4d1p7  42064  aks4d1p8  42068  primrootlekpowne0  42086  aks6d1c2p2  42100  sticksstones1  42127  mulgt0con1dlem  42463  nna4b4nsq  42646  naddwordnexlem4  43390  vk15.4j  44525  isosctrlem1ALT  44931  tworepnotupword  46839  n0nsn2el  46974  afvres  47121  otiunsndisjX  47228  fmtnoinf  47460  requad2  47547  copisnmnd  48012  dig1  48457  rrxsphere  48597