Theorem con3d 155

Description: A contraposition deduction. Deduction form of con3 156. (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 132	. . 3 ⊢ (¬ ¬ 𝜓 → 𝜓)
2		con3d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 34	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝜒))
4	3	con1d 147	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  156  con3rr3  158  nsyld  159  nsyli  160  mth8  163  pm5.21ndd  381  bija  382  con3dimp  409  orim12dALT  906  aleximi  1813  nelcon3d  3102  rexim  3205  spcimegf  3532  spcimedv  3537  rspcimedv  3561  ssneld  3891  sscon  4036  difrab  4197  disjord  4951  disjiund  4953  dtru  5162  otiunsndisj  5301  wereu2  5440  ndmfv  6568  dff3  6729  soisores  6943  releldmdifi  7600  funeldmdif  7603  ressuppssdif  7702  wfrlem10  7816  tz7.49  7932  oaord  8023  oalimcl  8036  omord2  8043  omcan  8045  omeulem1  8058  oeord  8064  oecan  8065  nnaord  8095  nnmord  8108  nneob  8129  omsmo  8131  domtriord  8510  isinf  8577  pssnn  8582  frfi  8609  fisupg  8612  difinf  8634  supmo  8762  infmo  8805  alephord  9347  fin17  9662  isfin7-2  9664  fin1a2lem12  9679  fpwwe2lem13  9910  prub  10262  genpnnp  10273  ltaddpr  10302  prlem936  10315  ltadd2  10591  ltord1  11014  ltmul1  11338  lt2msq  11373  nnge1  11513  nzadd  11879  zeo  11917  irradd  12222  irrmul  12223  mul2lt0bi  12345  supxrun  12559  supxrgtmnf  12572  ssfzoulel  12981  zesq  13437  bccmpl  13519  fundmge2nop0  13696  repswswrd  13982  s3iunsndisj  14162  lcmftp  15809  prm2orodd  15864  coprm  15884  prmndvdsfaclt  15896  hashgcdeq  15955  prmreclem3  16083  vdwnnlem2  16161  latnlej2  17510  mgm2nsgrplem3  17846  f1omvdco2  18307  oddvds  18406  gexdvds  18439  frgpnabl  18718  ablfac1eulem  18911  ablfac1eu  18912  psgnodpm  20414  obselocv  20554  1marepvmarrepid  20868  mdetunilem9  20913  t1connperf  21728  txindislem  21925  fbasrn  22176  isufil2  22200  ufileu  22211  filufint  22212  ufilen  22222  fin1aufil  22224  alexsubALTlem4  22342  ptcmplem2  22345  itg2gt0  24044  cosord  24797  argimgt0  24876  logdivlt  24885  logrec  25022  dcubic  25105  wilthlem2  25328  bposlem3  25544  dchrisum0fno1  25769  numedglnl  26612  nbumgr  26812  uhgrnbgr0nb  26819  cusgrfi  26923  vtxduhgr0nedg  26957  uhgrvd00  26999  wlkp1lem6  27145  2wspmdisj  27808  chnlen0  28912  staddi  29714  stadd3i  29716  strlem1  29718  atoml2i  29851  prmdvdsbc  30216  psgnfzto1stlem  30664  madjusmdetlem1  30707  madjusmdetlem2  30708  hasheuni  30961  sitgaddlemb  31223  eulerpartlemb  31243  ballotlemfc0  31367  ballotlemfcc  31368  acycgrislfgr  32008  umgracycusgr  32010  acycgrsubgr  32014  funeldmb  32615  dfon2lem6  32642  exnel  32657  frpomin  32688  sltres  32779  nosepssdm  32800  nosupbnd1lem1  32818  sletr  32847  nn0prpwlem  33280  waj-ax  33372  bj-dtru  33708  sucneqond  34196  wl-spae  34313  wl-ax11-lem3  34369  lindsadd  34435  matunitlindflem1  34438  poimirlem26  34468  poimirlem28  34470  poimirlem31  34473  areacirc  34537  pridlc3  34902  lkreqN  35856  atlrelat1  36007  2llnneN  36095  cdlemg4c  37298  mapdh8e  38470  sn-dtru  38660  vk15.4j  40420  isosctrlem1ALT  40826  afvres  42907  otiunsndisjX  43014  fmtnoinf  43200  requad2  43290  copisnmnd  43578  dig1  44169  rrxsphere  44236