Theorem con3d 153

Description: A contraposition deduction. Deduction form of con3 154. (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 131	. . 3 ⊢ (¬ ¬ 𝜓 → 𝜓)
2		con3d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 35	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝜒))
4	3	con1d 146	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  154  con3rr3  156  nsyld  157  nsyli  158  jcn  163  pm5.21ndd  382  bija  383  con3dimp  413  orim12dALT  924  aleximi  1860  nelcon3d  3066  spcimegf  3518  spcimedv  3553  rspcimedv  3571  ssneld  3938  sscon  4096  difrab  4270  disjord  5097  disjiund  5099  dtruALT2  5341  exneq  5417  otiunsndisj  5503  wereu2  5658  frpomin  6341  ndmfv  6913  dff3  7095  soisores  7325  funeldmb  7357  releldmdifi  8041  funeldmdif  8044  ressuppssdif  8180  tz7.49  8431  oaord  8531  oalimcl  8544  omord2  8551  omcan  8553  omeulem1  8566  oeord  8573  oecan  8574  nnaord  8604  nnmord  8617  nneob  8641  omsmo  8643  domtriord  9110  pssnn  9152  isinf  9224  frfi  9244  fisupg  9247  difinf  9270  supmo  9411  infmo  9456  alephord  10058  fin17  10377  isfin7-2  10379  fin1a2lem12  10394  fpwwe2lem12  10626  prub  10978  genpnnp  10989  ltaddpr  11018  prlem936  11031  ltadd2  11313  ltord1  11739  ltmul1  12064  lt2msq  12099  nnge1  12263  nzadd  12641  zeo  12681  irradd  12996  irrmul  12997  mul2lt0bi  13123  supxrun  13341  supxrgtmnf  13354  ssfzoulel  13789  zesq  14262  bccmpl  14345  fundmge2nop0  14539  repswswrd  14821  s3iunsndisj  15005  lcmftp  16693  prm2orodd  16748  coprm  16769  prmndvdsfaclt  16783  prmdvdsbc  16784  hashgcdeq  16848  prmreclem3  16977  vdwnnlem2  17055  latnlej2  18514  mgm2nsgrplem3  18981  f1omvdco2  19517  oddvds  19616  gexdvds  19653  frgpnabl  19944  ablfac1eulem  20143  ablfac1eu  20144  cmprmidlmcl  21454  psgnodpm  21717  obselocv  21857  1marepvmarrepid  22711  mdetunilem9  22756  t1connperf  23572  txindislem  23769  fbasrn  24020  isufil2  24044  ufileu  24055  filufint  24056  ufilen  24066  fin1aufil  24068  alexsubALTlem4  24186  ptcmplem2  24189  itg2gt0  25898  cosord  26672  argimgt0  26753  logdivlt  26762  logrec  26904  dcubic  26987  wilthlem2  27209  bposlem3  27426  dchrisum0fno1  27651  ltsres  27802  nosepssdm  27826  nosupbnd1lem1  27848  lestr  27902  om2noseqf1o  28470  numedglnl  29460  nbumgr  29663  uhgrnbgr0nb  29670  cusgrfi  29774  vtxduhgr0nedg  29808  uhgrvd00  29850  wlkp1lem6  29992  2wspmdisj  30654  chnlen0  31762  staddi  32564  stadd3i  32566  strlem1  32568  atoml2i  32701  n0nsnel  32827  psgnfzto1stlem  33386  madjusmdetlem1  34183  hasheuni  34441  sitgaddlemb  34704  eulerpartlemb  34724  ballotlemfc0  34849  ballotlemfcc  34850  cbvex1v  35428  onvf1odlem4  35556  acycgrislfgr  35610  umgracycusgr  35612  acycgrsubgr  35616  dfon2lem6  36244  exnel  36258  nn0prpwlem  36799  waj-ax  36891  dfttc4lem2  37006  sucneqond  37977  wl-spae  38142  lindsadd  38230  matunitlindflem1  38233  poimirlem26  38263  poimirlem28  38265  poimirlem31  38268  areacirc  38330  pridlc3  38690  lkreqN  39912  atlrelat1  40063  2llnneN  40151  cdlemg4c  41354  mapdh8e  42526  aks4d1p7  42818  aks4d1p8  42822  primrootlekpowne0  42840  aks6d1c2p2  42854  sticksstones1  42881  mulgt0con1dlem  43211  nna4b4nsq  43362  naddwordnexlem4  44098  vk15.4j  45207  isosctrlem1ALT  45612  n0nsn2el  47729  afvres  47876  otiunsndisjX  47983  fmtnoinf  48255  requad2  48355  cycldlenngric  48660  copisnmnd  48901  dig1  49355  rrxsphere  49495