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  3509  spcimedv  3550  rspcimedv  3568  ssneld  3936  sscon  4096  difrab  4271  disjord  5088  disjiund  5090  dtruALT2  5316  exneq  5386  otiunsndisj  5469  wereu2  5622  frpomin  6299  ndmfv  6867  dff3  7047  soisores  7275  funeldmb  7307  releldmdifi  7991  funeldmdif  7994  ressuppssdif  8129  tz7.49  8378  oaord  8476  oalimcl  8489  omord2  8496  omcan  8498  omeulem1  8511  oeord  8518  oecan  8519  nnaord  8549  nnmord  8562  nneob  8586  omsmo  8588  domtriord  9055  pssnn  9097  isinf  9169  frfi  9189  fisupg  9192  difinf  9215  supmo  9359  infmo  9404  alephord  9989  fin17  10308  isfin7-2  10310  fin1a2lem12  10325  fpwwe2lem12  10557  prub  10909  genpnnp  10920  ltaddpr  10949  prlem936  10962  ltadd2  11241  ltord1  11667  ltmul1  11995  lt2msq  12031  nnge1  12177  nzadd  12543  zeo  12582  irradd  12890  irrmul  12891  mul2lt0bi  13017  supxrun  13235  supxrgtmnf  13248  ssfzoulel  13680  zesq  14153  bccmpl  14236  fundmge2nop0  14429  repswswrd  14711  s3iunsndisj  14895  lcmftp  16567  prm2orodd  16622  coprm  16642  prmndvdsfaclt  16656  prmdvdsbc  16657  hashgcdeq  16721  prmreclem3  16850  vdwnnlem2  16928  latnlej2  18386  mgm2nsgrplem3  18849  f1omvdco2  19381  oddvds  19480  gexdvds  19517  frgpnabl  19808  ablfac1eulem  20007  ablfac1eu  20008  psgnodpm  21547  obselocv  21687  1marepvmarrepid  22523  mdetunilem9  22568  t1connperf  23384  txindislem  23581  fbasrn  23832  isufil2  23856  ufileu  23867  filufint  23868  ufilen  23878  fin1aufil  23880  alexsubALTlem4  23998  ptcmplem2  24001  itg2gt0  25721  cosord  26500  argimgt0  26581  logdivlt  26590  logrec  26733  dcubic  26816  wilthlem2  27039  bposlem3  27257  dchrisum0fno1  27482  sltres  27634  nosepssdm  27658  nosupbnd1lem1  27680  sletr  27734  om2noseqf1o  28282  numedglnl  29200  nbumgr  29403  uhgrnbgr0nb  29410  cusgrfi  29515  vtxduhgr0nedg  29549  uhgrvd00  29591  wlkp1lem6  29733  2wspmdisj  30395  chnlen0  31502  staddi  32304  stadd3i  32306  strlem1  32308  atoml2i  32441  n0nsnel  32572  psgnfzto1stlem  33163  madjusmdetlem1  33965  hasheuni  34223  sitgaddlemb  34486  eulerpartlemb  34506  ballotlemfc0  34631  ballotlemfcc  34632  cbvex1v  35211  onvf1odlem4  35281  acycgrislfgr  35327  umgracycusgr  35329  acycgrsubgr  35333  dfon2lem6  35961  exnel  35975  nn0prpwlem  36497  waj-ax  36589  sucneqond  37541  wl-spae  37697  lindsadd  37785  matunitlindflem1  37788  poimirlem26  37818  poimirlem28  37820  poimirlem31  37823  areacirc  37885  pridlc3  38245  lkreqN  39467  atlrelat1  39618  2llnneN  39706  cdlemg4c  40909  mapdh8e  42081  aks4d1p7  42374  aks4d1p8  42378  primrootlekpowne0  42396  aks6d1c2p2  42410  sticksstones1  42437  mulgt0con1dlem  42760  nna4b4nsq  42939  naddwordnexlem4  43679  vk15.4j  44805  isosctrlem1ALT  45210  n0nsn2el  47307  afvres  47454  otiunsndisjX  47561  fmtnoinf  47818  requad2  47905  cycldlenngric  48210  copisnmnd  48451  dig1  48890  rrxsphere  49030