Theorem con3d 153

Description: A contraposition deduction. Deduction form of con3 154. (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 131	. . 3 ⊢ (¬ ¬ 𝜓 → 𝜓)
2		con3d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 35	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝜒))
4	3	con1d 146	1 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  con3  154  con3rr3  156  nsyld  157  nsyli  158  jcn  163  pm5.21ndd  382  bija  383  con3dimp  414  orim12dALT  925  aleximi  1865  nelcon3d  3069  spcimegf  3518  spcimedv  3553  rspcimedv  3571  ssneld  3915  sscon  4082  difrab  4266  disjord  5095  disjiund  5097  dtruALT2  5336  exneq  5408  otiunsndisj  5497  wereu2  5652  frpomin  6361  ndmfv  6940  dff3  7124  soisores  7358  funeldmb  7392  releldmdifi  8081  funeldmdif  8084  ressuppssdif  8230  tz7.49  8483  oaord  8583  oalimcl  8596  omord2  8603  omcan  8605  omeulem1  8618  oeord  8625  oecan  8626  nnaord  8656  nnmord  8669  nneob  8693  omsmo  8695  domtriord  9170  pssnn  9212  isinf  9284  frfi  9304  fisupg  9307  difinf  9331  supmo  9471  infmo  9516  alephord  10181  fin17  10499  isfin7-2  10501  fin1a2lem12  10516  fpwwe2lem12  10754  prub  11106  genpnnp  11117  ltaddpr  11146  prlem936  11159  ltadd2  11441  ltord1  11869  ltmul1  12194  lt2msq  12229  nnge1  12393  nzadd  12771  zeo  12812  irradd  13128  irrmul  13129  mul2lt0bi  13255  supxrun  13473  supxrgtmnf  13486  ssfzoulel  13922  zesq  14397  bccmpl  14480  fundmge2nop0  14674  repswswrd  14963  s3iunsndisj  15150  lcmftp  16840  prm2orodd  16895  coprm  16916  prmndvdsfaclt  16930  prmdvdsbc  16931  hashgcdeq  16996  prmreclem3  17125  vdwnnlem2  17203  latnlej2  18662  mgm2nsgrplem3  19148  f1omvdco2  19692  oddvds  19791  gexdvds  19828  frgpnabl  20119  ablfac1eulem  20318  ablfac1eu  20319  cmprmidlmcl  21661  psgnodpm  21924  obselocv  22064  1marepvmarrepid  22920  mdetunilem9  22965  matunitlindflem1  23024  t1connperf  23784  txindislem  23982  fbasrn  24233  isufil2  24257  ufileu  24268  filufint  24269  ufilen  24279  fin1aufil  24281  alexsubALTlem4  24399  ptcmplem2  24402  itg2gt0  26111  cosord  26889  argimgt0  26970  logdivlt  26979  logrec  27121  dcubic  27204  wilthlem2  27426  bposlem3  27643  dchrisum0fno1  27868  ltsres  28049  nosepssdm  28073  nosupbnd1lem1  28095  lestr  28149  om2noseqf1o  28717  numedglnl  29752  nbumgr  29958  uhgrnbgr0nb  29965  cusgrfi  30069  vtxduhgr0nedg  30103  uhgrvd00  30145  wlkp1lem6  30287  2wspmdisj  30968  chnlen0  32076  staddi  32878  stadd3i  32880  strlem1  32882  atoml2i  33015  n0nsnel  33183  psgnfzto1stlem  33731  madjusmdetlem1  34529  hasheuni  34787  sitgaddlemb  35050  eulerpartlemb  35070  ballotlemfc0  35195  ballotlemfcc  35196  cbvex1v  35774  onvf1odlem4  36034  onprcf1acwevdlem1  36045  acycgrislfgr  36074  umgracycusgr  36076  acycgrsubgr  36080  dfon2lem6  36728  exnel  36742  nn0prpwlem  37288  waj-ax  37380  dfttc4lem2  37495  sucneqond  38480  wl-spae  38645  lindsadd  38728  poimirlem26  38756  poimirlem28  38758  poimirlem31  38761  areacirc  38823  pridlc3  39199  lkreqN  40419  atlrelat1  40570  2llnneN  40658  cdlemg4c  41861  mapdh8e  43033  aks4d1p7  43325  aks4d1p8  43329  primrootlekpowne0  43347  aks6d1c2p2  43361  sticksstones1  43388  mulgt0con1dlem  43726  naddwordnexlem4  44595  vk15.4j  45702  isosctrlem1ALT  46107  n0nsn2el  48300  afvres  48447  otiunsndisjX  48554  fmtnoinf  48826  requad2  48926  cycldlenngric  49231  copisnmnd  49471  dig1  49925  rrxsphere  50065