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  3034  spcimegf  3504  spcimedv  3548  rspcimedv  3566  ssneld  3934  sscon  4091  difrab  4266  disjord  5078  disjiund  5080  dtruALT2  5306  exneq  5376  otiunsndisj  5458  wereu2  5611  frpomin  6283  ndmfv  6849  dff3  7028  soisores  7256  funeldmb  7288  releldmdifi  7972  funeldmdif  7975  ressuppssdif  8110  tz7.49  8359  oaord  8457  oalimcl  8470  omord2  8477  omcan  8479  omeulem1  8492  oeord  8498  oecan  8499  nnaord  8529  nnmord  8542  nneob  8566  omsmo  8568  domtriord  9031  pssnn  9073  isinf  9144  frfi  9164  fisupg  9167  difinf  9190  supmo  9331  infmo  9376  alephord  9958  fin17  10277  isfin7-2  10279  fin1a2lem12  10294  fpwwe2lem12  10525  prub  10877  genpnnp  10888  ltaddpr  10917  prlem936  10930  ltadd2  11209  ltord1  11635  ltmul1  11963  lt2msq  11999  nnge1  12145  nzadd  12512  zeo  12551  irradd  12863  irrmul  12864  mul2lt0bi  12990  supxrun  13207  supxrgtmnf  13220  ssfzoulel  13652  zesq  14125  bccmpl  14208  fundmge2nop0  14401  repswswrd  14683  s3iunsndisj  14867  lcmftp  16539  prm2orodd  16594  coprm  16614  prmndvdsfaclt  16628  prmdvdsbc  16629  hashgcdeq  16693  prmreclem3  16822  vdwnnlem2  16900  latnlej2  18357  mgm2nsgrplem3  18820  f1omvdco2  19353  oddvds  19452  gexdvds  19489  frgpnabl  19780  ablfac1eulem  19979  ablfac1eu  19980  psgnodpm  21518  obselocv  21658  1marepvmarrepid  22483  mdetunilem9  22528  t1connperf  23344  txindislem  23541  fbasrn  23792  isufil2  23816  ufileu  23827  filufint  23828  ufilen  23838  fin1aufil  23840  alexsubALTlem4  23958  ptcmplem2  23961  itg2gt0  25681  cosord  26460  argimgt0  26541  logdivlt  26550  logrec  26693  dcubic  26776  wilthlem2  26999  bposlem3  27217  dchrisum0fno1  27442  sltres  27594  nosepssdm  27618  nosupbnd1lem1  27640  sletr  27690  om2noseqf1o  28224  numedglnl  29115  nbumgr  29318  uhgrnbgr0nb  29325  cusgrfi  29430  vtxduhgr0nedg  29464  uhgrvd00  29506  wlkp1lem6  29648  2wspmdisj  30307  chnlen0  31414  staddi  32216  stadd3i  32218  strlem1  32220  atoml2i  32353  n0nsnel  32485  psgnfzto1stlem  33059  madjusmdetlem1  33830  hasheuni  34088  sitgaddlemb  34351  eulerpartlemb  34371  ballotlemfc0  34496  ballotlemfcc  34497  cbvex1v  35076  onvf1odlem4  35118  acycgrislfgr  35164  umgracycusgr  35166  acycgrsubgr  35170  dfon2lem6  35801  exnel  35815  nn0prpwlem  36335  waj-ax  36427  sucneqond  37378  wl-spae  37534  wl-ax11-lem3  37600  lindsadd  37632  matunitlindflem1  37635  poimirlem26  37665  poimirlem28  37667  poimirlem31  37670  areacirc  37732  pridlc3  38092  lkreqN  39188  atlrelat1  39339  2llnneN  39427  cdlemg4c  40630  mapdh8e  41802  aks4d1p7  42095  aks4d1p8  42099  primrootlekpowne0  42117  aks6d1c2p2  42131  sticksstones1  42158  mulgt0con1dlem  42481  nna4b4nsq  42672  naddwordnexlem4  43413  vk15.4j  44540  isosctrlem1ALT  44945  n0nsn2el  47035  afvres  47182  otiunsndisjX  47289  fmtnoinf  47546  requad2  47633  cycldlenngric  47938  copisnmnd  48179  dig1  48619  rrxsphere  48759