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  912  aleximi  1834  nelcon3d  3041  spcimegf  3497  spcimedv  3538  rspcimedv  3556  ssneld  3924  sscon  4084  difrab  4259  disjord  5075  disjiund  5077  dtruALT2  5305  exneq  5381  otiunsndisj  5466  wereu2  5619  frpomin  6296  ndmfv  6864  dff3  7044  soisores  7273  funeldmb  7305  releldmdifi  7989  funeldmdif  7992  ressuppssdif  8126  tz7.49  8375  oaord  8473  oalimcl  8486  omord2  8493  omcan  8495  omeulem1  8508  oeord  8515  oecan  8516  nnaord  8546  nnmord  8559  nneob  8583  omsmo  8585  domtriord  9052  pssnn  9094  isinf  9166  frfi  9186  fisupg  9189  difinf  9212  supmo  9356  infmo  9401  alephord  9986  fin17  10305  isfin7-2  10307  fin1a2lem12  10322  fpwwe2lem12  10554  prub  10906  genpnnp  10917  ltaddpr  10946  prlem936  10959  ltadd2  11239  ltord1  11665  ltmul1  11994  lt2msq  12030  nnge1  12194  nzadd  12564  zeo  12604  irradd  12912  irrmul  12913  mul2lt0bi  13039  supxrun  13257  supxrgtmnf  13270  ssfzoulel  13704  zesq  14177  bccmpl  14260  fundmge2nop0  14453  repswswrd  14735  s3iunsndisj  14919  lcmftp  16594  prm2orodd  16649  coprm  16670  prmndvdsfaclt  16684  prmdvdsbc  16685  hashgcdeq  16749  prmreclem3  16878  vdwnnlem2  16956  latnlej2  18414  mgm2nsgrplem3  18880  f1omvdco2  19412  oddvds  19511  gexdvds  19548  frgpnabl  19839  ablfac1eulem  20038  ablfac1eu  20039  psgnodpm  21576  obselocv  21716  1marepvmarrepid  22549  mdetunilem9  22594  t1connperf  23410  txindislem  23607  fbasrn  23858  isufil2  23882  ufileu  23893  filufint  23894  ufilen  23904  fin1aufil  23906  alexsubALTlem4  24024  ptcmplem2  24027  itg2gt0  25736  cosord  26511  argimgt0  26592  logdivlt  26601  logrec  26744  dcubic  26827  wilthlem2  27050  bposlem3  27268  dchrisum0fno1  27493  ltsres  27645  nosepssdm  27669  nosupbnd1lem1  27691  lestr  27745  om2noseqf1o  28312  numedglnl  29232  nbumgr  29435  uhgrnbgr0nb  29442  cusgrfi  29547  vtxduhgr0nedg  29581  uhgrvd00  29623  wlkp1lem6  29765  2wspmdisj  30427  chnlen0  31535  staddi  32337  stadd3i  32339  strlem1  32341  atoml2i  32474  n0nsnel  32605  psgnfzto1stlem  33181  madjusmdetlem1  33992  hasheuni  34250  sitgaddlemb  34513  eulerpartlemb  34533  ballotlemfc0  34658  ballotlemfcc  34659  cbvex1v  35237  onvf1odlem4  35309  acycgrislfgr  35355  umgracycusgr  35357  acycgrsubgr  35361  dfon2lem6  35989  exnel  36003  nn0prpwlem  36525  waj-ax  36617  dfttc4lem2  36732  sucneqond  37692  wl-spae  37857  lindsadd  37945  matunitlindflem1  37948  poimirlem26  37978  poimirlem28  37980  poimirlem31  37983  areacirc  38045  pridlc3  38405  lkreqN  39627  atlrelat1  39778  2llnneN  39866  cdlemg4c  41069  mapdh8e  42241  aks4d1p7  42533  aks4d1p8  42537  primrootlekpowne0  42555  aks6d1c2p2  42569  sticksstones1  42596  mulgt0con1dlem  42925  nna4b4nsq  43104  naddwordnexlem4  43844  vk15.4j  44970  isosctrlem1ALT  45375  n0nsn2el  47470  afvres  47617  otiunsndisjX  47724  fmtnoinf  47996  requad2  48096  cycldlenngric  48401  copisnmnd  48642  dig1  49081  rrxsphere  49221