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  3510  spcimedv  3551  rspcimedv  3569  ssneld  3937  sscon  4097  difrab  4272  disjord  5089  disjiund  5091  dtruALT2  5317  exneq  5392  otiunsndisj  5476  wereu2  5629  frpomin  6306  ndmfv  6874  dff3  7054  soisores  7283  funeldmb  7315  releldmdifi  7999  funeldmdif  8002  ressuppssdif  8137  tz7.49  8386  oaord  8484  oalimcl  8497  omord2  8504  omcan  8506  omeulem1  8519  oeord  8526  oecan  8527  nnaord  8557  nnmord  8570  nneob  8594  omsmo  8596  domtriord  9063  pssnn  9105  isinf  9177  frfi  9197  fisupg  9200  difinf  9223  supmo  9367  infmo  9412  alephord  9997  fin17  10316  isfin7-2  10318  fin1a2lem12  10333  fpwwe2lem12  10565  prub  10917  genpnnp  10928  ltaddpr  10957  prlem936  10970  ltadd2  11249  ltord1  11675  ltmul1  12003  lt2msq  12039  nnge1  12185  nzadd  12551  zeo  12590  irradd  12898  irrmul  12899  mul2lt0bi  13025  supxrun  13243  supxrgtmnf  13256  ssfzoulel  13688  zesq  14161  bccmpl  14244  fundmge2nop0  14437  repswswrd  14719  s3iunsndisj  14903  lcmftp  16575  prm2orodd  16630  coprm  16650  prmndvdsfaclt  16664  prmdvdsbc  16665  hashgcdeq  16729  prmreclem3  16858  vdwnnlem2  16936  latnlej2  18394  mgm2nsgrplem3  18857  f1omvdco2  19389  oddvds  19488  gexdvds  19525  frgpnabl  19816  ablfac1eulem  20015  ablfac1eu  20016  psgnodpm  21555  obselocv  21695  1marepvmarrepid  22531  mdetunilem9  22576  t1connperf  23392  txindislem  23589  fbasrn  23840  isufil2  23864  ufileu  23875  filufint  23876  ufilen  23886  fin1aufil  23888  alexsubALTlem4  24006  ptcmplem2  24009  itg2gt0  25729  cosord  26508  argimgt0  26589  logdivlt  26598  logrec  26741  dcubic  26824  wilthlem2  27047  bposlem3  27265  dchrisum0fno1  27490  ltsres  27642  nosepssdm  27666  nosupbnd1lem1  27688  lestr  27742  om2noseqf1o  28309  numedglnl  29229  nbumgr  29432  uhgrnbgr0nb  29439  cusgrfi  29544  vtxduhgr0nedg  29578  uhgrvd00  29620  wlkp1lem6  29762  2wspmdisj  30424  chnlen0  31531  staddi  32333  stadd3i  32335  strlem1  32337  atoml2i  32470  n0nsnel  32601  psgnfzto1stlem  33193  madjusmdetlem1  34004  hasheuni  34262  sitgaddlemb  34525  eulerpartlemb  34545  ballotlemfc0  34670  ballotlemfcc  34671  cbvex1v  35249  onvf1odlem4  35319  acycgrislfgr  35365  umgracycusgr  35367  acycgrsubgr  35371  dfon2lem6  35999  exnel  36013  nn0prpwlem  36535  waj-ax  36627  sucneqond  37609  wl-spae  37765  lindsadd  37853  matunitlindflem1  37856  poimirlem26  37886  poimirlem28  37888  poimirlem31  37891  areacirc  37953  pridlc3  38313  lkreqN  39535  atlrelat1  39686  2llnneN  39774  cdlemg4c  40977  mapdh8e  42149  aks4d1p7  42442  aks4d1p8  42446  primrootlekpowne0  42464  aks6d1c2p2  42478  sticksstones1  42505  mulgt0con1dlem  42828  nna4b4nsq  43007  naddwordnexlem4  43747  vk15.4j  44873  isosctrlem1ALT  45278  n0nsn2el  47374  afvres  47521  otiunsndisjX  47628  fmtnoinf  47885  requad2  47972  cycldlenngric  48277  copisnmnd  48518  dig1  48957  rrxsphere  49097