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  1855  nelcon3d  3068  spcimegf  3522  spcimedv  3557  rspcimedv  3575  ssneld  3941  sscon  4099  difrab  4273  disjord  5094  disjiund  5096  dtruALT2  5332  exneq  5408  otiunsndisj  5494  wereu2  5649  frpomin  6331  ndmfv  6903  dff3  7085  soisores  7315  funeldmb  7347  releldmdifi  8030  funeldmdif  8033  ressuppssdif  8169  tz7.49  8420  oaord  8520  oalimcl  8533  omord2  8540  omcan  8542  omeulem1  8555  oeord  8562  oecan  8563  nnaord  8593  nnmord  8606  nneob  8630  omsmo  8632  domtriord  9099  pssnn  9141  isinf  9213  frfi  9233  fisupg  9236  difinf  9259  supmo  9400  infmo  9445  alephord  10047  fin17  10366  isfin7-2  10368  fin1a2lem12  10383  fpwwe2lem12  10615  prub  10967  genpnnp  10978  ltaddpr  11007  prlem936  11020  ltadd2  11302  ltord1  11728  ltmul1  12056  lt2msq  12091  nnge1  12255  nzadd  12633  zeo  12673  irradd  12988  irrmul  12989  mul2lt0bi  13115  supxrun  13333  supxrgtmnf  13346  ssfzoulel  13780  zesq  14253  bccmpl  14336  fundmge2nop0  14529  repswswrd  14811  s3iunsndisj  14995  lcmftp  16684  prm2orodd  16739  coprm  16760  prmndvdsfaclt  16774  prmdvdsbc  16775  hashgcdeq  16839  prmreclem3  16968  vdwnnlem2  17046  latnlej2  18505  mgm2nsgrplem3  18972  f1omvdco2  19509  oddvds  19608  gexdvds  19645  frgpnabl  19936  ablfac1eulem  20135  ablfac1eu  20136  psgnodpm  21698  obselocv  21838  1marepvmarrepid  22693  mdetunilem9  22738  t1connperf  23554  txindislem  23751  fbasrn  24002  isufil2  24026  ufileu  24037  filufint  24038  ufilen  24048  fin1aufil  24050  alexsubALTlem4  24168  ptcmplem2  24171  itg2gt0  25880  cosord  26654  argimgt0  26735  logdivlt  26744  logrec  26886  dcubic  26969  wilthlem2  27191  bposlem3  27408  dchrisum0fno1  27633  ltsres  27784  nosepssdm  27808  nosupbnd1lem1  27830  lestr  27884  om2noseqf1o  28452  numedglnl  29403  nbumgr  29606  uhgrnbgr0nb  29613  cusgrfi  29717  vtxduhgr0nedg  29751  uhgrvd00  29793  wlkp1lem6  29935  2wspmdisj  30597  chnlen0  31705  staddi  32507  stadd3i  32509  strlem1  32511  atoml2i  32644  n0nsnel  32771  psgnfzto1stlem  33333  madjusmdetlem1  34134  hasheuni  34392  sitgaddlemb  34655  eulerpartlemb  34675  ballotlemfc0  34800  ballotlemfcc  34801  cbvex1v  35379  onvf1odlem4  35461  acycgrislfgr  35515  umgracycusgr  35517  acycgrsubgr  35521  dfon2lem6  36149  exnel  36163  nn0prpwlem  36695  waj-ax  36787  dfttc4lem2  36902  sucneqond  37871  wl-spae  38036  lindsadd  38124  matunitlindflem1  38127  poimirlem26  38157  poimirlem28  38159  poimirlem31  38162  areacirc  38224  pridlc3  38584  lkreqN  39806  atlrelat1  39957  2llnneN  40045  cdlemg4c  41248  mapdh8e  42420  aks4d1p7  42712  aks4d1p8  42716  primrootlekpowne0  42734  aks6d1c2p2  42748  sticksstones1  42775  mulgt0con1dlem  43103  nna4b4nsq  43254  naddwordnexlem4  43990  vk15.4j  45102  isosctrlem1ALT  45507  n0nsn2el  47617  afvres  47764  otiunsndisjX  47871  fmtnoinf  48143  requad2  48243  cycldlenngric  48548  copisnmnd  48789  dig1  49239  rrxsphere  49379