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  3038  spcimegf  3506  spcimedv  3547  rspcimedv  3565  ssneld  3933  sscon  4094  difrab  4269  disjord  5084  disjiund  5086  dtruALT2  5312  exneq  5382  otiunsndisj  5465  wereu2  5618  frpomin  6295  ndmfv  6863  dff3  7042  soisores  7270  funeldmb  7302  releldmdifi  7986  funeldmdif  7989  ressuppssdif  8124  tz7.49  8373  oaord  8471  oalimcl  8484  omord2  8491  omcan  8493  omeulem1  8506  oeord  8512  oecan  8513  nnaord  8543  nnmord  8556  nneob  8580  omsmo  8582  domtriord  9046  pssnn  9088  isinf  9159  frfi  9179  fisupg  9182  difinf  9205  supmo  9346  infmo  9391  alephord  9976  fin17  10295  isfin7-2  10297  fin1a2lem12  10312  fpwwe2lem12  10543  prub  10895  genpnnp  10906  ltaddpr  10935  prlem936  10948  ltadd2  11227  ltord1  11653  ltmul1  11981  lt2msq  12017  nnge1  12163  nzadd  12530  zeo  12569  irradd  12881  irrmul  12882  mul2lt0bi  13008  supxrun  13225  supxrgtmnf  13238  ssfzoulel  13670  zesq  14143  bccmpl  14226  fundmge2nop0  14419  repswswrd  14701  s3iunsndisj  14885  lcmftp  16557  prm2orodd  16612  coprm  16632  prmndvdsfaclt  16646  prmdvdsbc  16647  hashgcdeq  16711  prmreclem3  16840  vdwnnlem2  16918  latnlej2  18375  mgm2nsgrplem3  18838  f1omvdco2  19370  oddvds  19469  gexdvds  19506  frgpnabl  19797  ablfac1eulem  19996  ablfac1eu  19997  psgnodpm  21535  obselocv  21675  1marepvmarrepid  22500  mdetunilem9  22545  t1connperf  23361  txindislem  23558  fbasrn  23809  isufil2  23833  ufileu  23844  filufint  23845  ufilen  23855  fin1aufil  23857  alexsubALTlem4  23975  ptcmplem2  23978  itg2gt0  25698  cosord  26477  argimgt0  26558  logdivlt  26567  logrec  26710  dcubic  26793  wilthlem2  27016  bposlem3  27234  dchrisum0fno1  27459  sltres  27611  nosepssdm  27635  nosupbnd1lem1  27657  sletr  27707  om2noseqf1o  28241  numedglnl  29133  nbumgr  29336  uhgrnbgr0nb  29343  cusgrfi  29448  vtxduhgr0nedg  29482  uhgrvd00  29524  wlkp1lem6  29666  2wspmdisj  30328  chnlen0  31435  staddi  32237  stadd3i  32239  strlem1  32241  atoml2i  32374  n0nsnel  32506  psgnfzto1stlem  33080  madjusmdetlem1  33851  hasheuni  34109  sitgaddlemb  34372  eulerpartlemb  34392  ballotlemfc0  34517  ballotlemfcc  34518  cbvex1v  35097  onvf1odlem4  35161  acycgrislfgr  35207  umgracycusgr  35209  acycgrsubgr  35213  dfon2lem6  35841  exnel  35855  nn0prpwlem  36377  waj-ax  36469  sucneqond  37420  wl-spae  37576  lindsadd  37663  matunitlindflem1  37666  poimirlem26  37696  poimirlem28  37698  poimirlem31  37701  areacirc  37763  pridlc3  38123  lkreqN  39279  atlrelat1  39430  2llnneN  39518  cdlemg4c  40721  mapdh8e  41893  aks4d1p7  42186  aks4d1p8  42190  primrootlekpowne0  42208  aks6d1c2p2  42222  sticksstones1  42249  mulgt0con1dlem  42577  nna4b4nsq  42768  naddwordnexlem4  43508  vk15.4j  44635  isosctrlem1ALT  45040  n0nsn2el  47139  afvres  47286  otiunsndisjX  47393  fmtnoinf  47650  requad2  47737  cycldlenngric  48042  copisnmnd  48283  dig1  48723  rrxsphere  48863