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  378  bija  379  con3dimp  407  orim12dALT  909  aleximi  1827  nelcon3d  3040  spcimegf  3576  spcimedv  3581  rspcimedv  3599  ssneld  3981  sscon  4138  difrab  4310  disjord  5141  disjiund  5143  dtruALT2  5374  exneq  5441  dtruOLD  5447  otiunsndisj  5526  wereu2  5679  frpomin  6353  ndmfv  6936  dff3  7114  soisores  7339  funeldmb  7371  releldmdifi  8059  funeldmdif  8062  ressuppssdif  8199  wfrlem10OLD  8348  tz7.49  8475  oaord  8577  oalimcl  8590  omord2  8597  omcan  8599  omeulem1  8612  oeord  8618  oecan  8619  nnaord  8649  nnmord  8662  nneob  8686  omsmo  8688  domtriord  9161  pssnn  9206  isinf  9294  isinfOLD  9295  pssnnOLD  9299  frfi  9322  fisupg  9325  difinf  9351  supmo  9495  infmo  9538  alephord  10118  fin17  10437  isfin7-2  10439  fin1a2lem12  10454  fpwwe2lem12  10685  prub  11037  genpnnp  11048  ltaddpr  11077  prlem936  11090  ltadd2  11368  ltord1  11790  ltmul1  12115  lt2msq  12151  nnge1  12292  nzadd  12662  zeo  12700  irradd  13009  irrmul  13010  mul2lt0bi  13134  supxrun  13349  supxrgtmnf  13362  ssfzoulel  13780  zesq  14243  bccmpl  14326  fundmge2nop0  14511  repswswrd  14792  s3iunsndisj  14973  lcmftp  16637  prm2orodd  16692  coprm  16712  prmndvdsfaclt  16727  prmdvdsbc  16728  hashgcdeq  16791  prmreclem3  16920  vdwnnlem2  16998  latnlej2  18484  mgm2nsgrplem3  18910  f1omvdco2  19446  oddvds  19545  gexdvds  19582  frgpnabl  19873  ablfac1eulem  20072  ablfac1eu  20073  psgnodpm  21584  obselocv  21726  1marepvmarrepid  22568  mdetunilem9  22613  t1connperf  23431  txindislem  23628  fbasrn  23879  isufil2  23903  ufileu  23914  filufint  23915  ufilen  23925  fin1aufil  23927  alexsubALTlem4  24045  ptcmplem2  24048  itg2gt0  25781  cosord  26558  argimgt0  26639  logdivlt  26648  logrec  26791  dcubic  26874  wilthlem2  27097  bposlem3  27315  dchrisum0fno1  27540  sltres  27692  nosepssdm  27716  nosupbnd1lem1  27738  sletr  27788  om2noseqf1o  28275  numedglnl  29080  nbumgr  29283  uhgrnbgr0nb  29290  cusgrfi  29395  vtxduhgr0nedg  29429  uhgrvd00  29471  wlkp1lem6  29615  2wspmdisj  30270  chnlen0  31377  staddi  32179  stadd3i  32181  strlem1  32183  atoml2i  32316  n0nsnel  32441  psgnfzto1stlem  32978  madjusmdetlem1  33642  madjusmdetlem2  33643  hasheuni  33918  sitgaddlemb  34182  eulerpartlemb  34202  ballotlemfc0  34326  ballotlemfcc  34327  acycgrislfgr  34980  umgracycusgr  34982  acycgrsubgr  34986  dfon2lem6  35612  exnel  35626  nn0prpwlem  36034  waj-ax  36126  sucneqond  37072  wl-spae  37216  wl-ax11-lem3  37282  lindsadd  37314  matunitlindflem1  37317  poimirlem26  37347  poimirlem28  37349  poimirlem31  37352  areacirc  37414  pridlc3  37774  lkreqN  38868  atlrelat1  39019  2llnneN  39108  cdlemg4c  40311  mapdh8e  41483  aks4d1p7  41782  aks4d1p8  41786  primrootlekpowne0  41803  aks6d1c2p2  41817  sticksstones1  41844  mulgt0con1dlem  42237  nna4b4nsq  42314  naddwordnexlem4  43068  vk15.4j  44204  isosctrlem1ALT  44610  tworepnotupword  46505  n0nsn2el  46640  afvres  46785  otiunsndisjX  46892  fmtnoinf  47108  requad2  47195  copisnmnd  47546  dig1  47996  rrxsphere  48136