Theorem con3d 621

Description: A contraposition deduction. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 31-Jan-2015.)

Hypothesis

Ref	Expression
con3d.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
con3d	⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))

Proof of Theorem con3d

Step	Hyp	Ref	Expression
1		con3d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		notnot 619	. . 3 ⊢ (𝜒 → ¬ ¬ 𝜒)
3	1, 2	syl6 33	. 2 ⊢ (𝜑 → (𝜓 → ¬ ¬ 𝜒))
4	3	con2d 614	1 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 604  ax-in2 605

This theorem is referenced by:  con3rr3  623  con3dimp  625  con3  632  nsyld  638  nsyli  639  jcn  641  notbi  656  impidc  844  bijadc  868  pm2.13dc  871  xoranor  1356  mo2n  2028  necon3ad  2351  necon3bd  2352  nelcon3d  2415  ssneld  3104  sscon  3215  difrab  3355  eunex  4484  ndmfvg  5460  nnaord  6413  nnmord  6421  php5  6760  php5dom  6765  supmoti  6888  exmidomniim  7021  mkvprop  7040  enmkvlem  7043  prubl  7318  letr  7871  eqord1  8269  cnstab  8431  prodge0  8636  lt2msq  8668  nnge1  8767  nzadd  9130  irradd  9465  irrmul  9466  xrletr  9621  frec2uzf1od  10210  zesq  10441  expcanlem  10493  nn0opthd  10500  bccmpl  10532  maxleast  11017  fisumss  11193  dvdsbnd  11681  prm2orodd  11843  coprm  11858  prmndvdsfaclt  11870  hashgcdeq  11940  cos11  12982  bj-nnsn  13116  bj-nnelirr  13322  exmid1stab  13368  ismkvnnlem  13419