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  381  bija  382  con3dimp  410  orim12dALT  911  aleximi  1835  nelcon3d  3051  spcimegf  3581  spcimedv  3586  rspcimedv  3604  ssneld  3985  sscon  4139  difrab  4309  disjord  5137  disjiund  5139  dtruALT2  5369  exneq  5436  dtruOLD  5442  otiunsndisj  5521  wereu2  5674  frpomin  6342  ndmfv  6927  dff3  7102  soisores  7324  funeldmb  7356  releldmdifi  8031  funeldmdif  8034  ressuppssdif  8170  wfrlem10OLD  8318  tz7.49  8445  oaord  8547  oalimcl  8560  omord2  8567  omcan  8569  omeulem1  8582  oeord  8588  oecan  8589  nnaord  8619  nnmord  8632  nneob  8655  omsmo  8657  domtriord  9123  pssnn  9168  isinf  9260  isinfOLD  9261  pssnnOLD  9265  frfi  9288  fisupg  9291  difinf  9316  supmo  9447  infmo  9490  alephord  10070  fin17  10389  isfin7-2  10391  fin1a2lem12  10406  fpwwe2lem12  10637  prub  10989  genpnnp  11000  ltaddpr  11029  prlem936  11042  ltadd2  11318  ltord1  11740  ltmul1  12064  lt2msq  12099  nnge1  12240  nzadd  12610  zeo  12648  irradd  12957  irrmul  12958  mul2lt0bi  13080  supxrun  13295  supxrgtmnf  13308  ssfzoulel  13726  zesq  14189  bccmpl  14269  fundmge2nop0  14453  repswswrd  14734  s3iunsndisj  14915  lcmftp  16573  prm2orodd  16628  coprm  16648  prmndvdsfaclt  16662  hashgcdeq  16722  prmreclem3  16851  vdwnnlem2  16929  latnlej2  18412  mgm2nsgrplem3  18801  f1omvdco2  19316  oddvds  19415  gexdvds  19452  frgpnabl  19743  ablfac1eulem  19942  ablfac1eu  19943  psgnodpm  21141  obselocv  21283  1marepvmarrepid  22077  mdetunilem9  22122  t1connperf  22940  txindislem  23137  fbasrn  23388  isufil2  23412  ufileu  23423  filufint  23424  ufilen  23434  fin1aufil  23436  alexsubALTlem4  23554  ptcmplem2  23557  itg2gt0  25278  cosord  26040  argimgt0  26120  logdivlt  26129  logrec  26268  dcubic  26351  wilthlem2  26573  bposlem3  26789  dchrisum0fno1  27014  sltres  27165  nosepssdm  27189  nosupbnd1lem1  27211  sletr  27261  numedglnl  28404  nbumgr  28604  uhgrnbgr0nb  28611  cusgrfi  28715  vtxduhgr0nedg  28749  uhgrvd00  28791  wlkp1lem6  28935  2wspmdisj  29590  chnlen0  30697  staddi  31499  stadd3i  31501  strlem1  31503  atoml2i  31636  prmdvdsbc  32022  psgnfzto1stlem  32259  madjusmdetlem1  32807  madjusmdetlem2  32808  hasheuni  33083  sitgaddlemb  33347  eulerpartlemb  33367  ballotlemfc0  33491  ballotlemfcc  33492  acycgrislfgr  34143  umgracycusgr  34145  acycgrsubgr  34149  dfon2lem6  34760  exnel  34774  nn0prpwlem  35207  waj-ax  35299  sucneqond  36246  wl-spae  36390  wl-ax11-lem3  36449  lindsadd  36481  matunitlindflem1  36484  poimirlem26  36514  poimirlem28  36516  poimirlem31  36519  areacirc  36581  pridlc3  36941  lkreqN  38040  atlrelat1  38191  2llnneN  38280  cdlemg4c  39483  mapdh8e  40655  aks4d1p7  40948  aks4d1p8  40952  aks6d1c2p2  40957  sticksstones1  40962  mulgt0con1dlem  41330  nna4b4nsq  41402  naddwordnexlem4  42152  vk15.4j  43289  isosctrlem1ALT  43695  tworepnotupword  45600  n0nsn2el  45735  afvres  45880  otiunsndisjX  45987  fmtnoinf  46204  requad2  46291  copisnmnd  46579  dig1  47294  rrxsphere  47434