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  1832  nelcon3d  3050  spcimegf  3551  spcimedv  3595  rspcimedv  3613  ssneld  3985  sscon  4143  difrab  4318  disjord  5132  disjiund  5134  dtruALT2  5370  exneq  5440  dtruOLD  5446  otiunsndisj  5525  wereu2  5682  frpomin  6361  ndmfv  6941  dff3  7120  soisores  7347  funeldmb  7379  releldmdifi  8070  funeldmdif  8073  ressuppssdif  8210  wfrlem10OLD  8358  tz7.49  8485  oaord  8585  oalimcl  8598  omord2  8605  omcan  8607  omeulem1  8620  oeord  8626  oecan  8627  nnaord  8657  nnmord  8670  nneob  8694  omsmo  8696  domtriord  9163  pssnn  9208  isinf  9296  isinfOLD  9297  frfi  9321  fisupg  9324  difinf  9349  supmo  9492  infmo  9535  alephord  10115  fin17  10434  isfin7-2  10436  fin1a2lem12  10451  fpwwe2lem12  10682  prub  11034  genpnnp  11045  ltaddpr  11074  prlem936  11087  ltadd2  11365  ltord1  11789  ltmul1  12117  lt2msq  12153  nnge1  12294  nzadd  12665  zeo  12704  irradd  13015  irrmul  13016  mul2lt0bi  13141  supxrun  13358  supxrgtmnf  13371  ssfzoulel  13799  zesq  14265  bccmpl  14348  fundmge2nop0  14541  repswswrd  14822  s3iunsndisj  15007  lcmftp  16673  prm2orodd  16728  coprm  16748  prmndvdsfaclt  16762  prmdvdsbc  16763  hashgcdeq  16827  prmreclem3  16956  vdwnnlem2  17034  latnlej2  18504  mgm2nsgrplem3  18933  f1omvdco2  19466  oddvds  19565  gexdvds  19602  frgpnabl  19893  ablfac1eulem  20092  ablfac1eu  20093  psgnodpm  21606  obselocv  21748  1marepvmarrepid  22581  mdetunilem9  22626  t1connperf  23444  txindislem  23641  fbasrn  23892  isufil2  23916  ufileu  23927  filufint  23928  ufilen  23938  fin1aufil  23940  alexsubALTlem4  24058  ptcmplem2  24061  itg2gt0  25795  cosord  26573  argimgt0  26654  logdivlt  26663  logrec  26806  dcubic  26889  wilthlem2  27112  bposlem3  27330  dchrisum0fno1  27555  sltres  27707  nosepssdm  27731  nosupbnd1lem1  27753  sletr  27803  om2noseqf1o  28307  numedglnl  29161  nbumgr  29364  uhgrnbgr0nb  29371  cusgrfi  29476  vtxduhgr0nedg  29510  uhgrvd00  29552  wlkp1lem6  29696  2wspmdisj  30356  chnlen0  31463  staddi  32265  stadd3i  32267  strlem1  32269  atoml2i  32402  n0nsnel  32534  psgnfzto1stlem  33120  madjusmdetlem1  33826  hasheuni  34086  sitgaddlemb  34350  eulerpartlemb  34370  ballotlemfc0  34495  ballotlemfcc  34496  cbvex1v  35088  acycgrislfgr  35157  umgracycusgr  35159  acycgrsubgr  35163  dfon2lem6  35789  exnel  35803  nn0prpwlem  36323  waj-ax  36415  sucneqond  37366  wl-spae  37522  wl-ax11-lem3  37588  lindsadd  37620  matunitlindflem1  37623  poimirlem26  37653  poimirlem28  37655  poimirlem31  37658  areacirc  37720  pridlc3  38080  lkreqN  39171  atlrelat1  39322  2llnneN  39411  cdlemg4c  40614  mapdh8e  41786  aks4d1p7  42084  aks4d1p8  42088  primrootlekpowne0  42106  aks6d1c2p2  42120  sticksstones1  42147  mulgt0con1dlem  42487  nna4b4nsq  42670  naddwordnexlem4  43414  vk15.4j  44548  isosctrlem1ALT  44954  tworepnotupword  46901  n0nsn2el  47037  afvres  47184  otiunsndisjX  47291  fmtnoinf  47523  requad2  47610  copisnmnd  48085  dig1  48529  rrxsphere  48669