Theorem con3d 640

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 638	. . 3 ⊢ (𝜒 → ¬ ¬ 𝜒)
3	1, 2	syl6 33	. 2 ⊢ (𝜑 → (𝜓 → ¬ ¬ 𝜒))
4	3	con2d 633	1 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3rr3  642  con3dimp  644  con3  651  nsyld  657  nsyli  658  jcn  661  notbi  676  impidc  870  bijadc  894  pm2.13dc  897  xoranor  1426  mo2n  2114  necon3ad  2462  necon3bd  2463  nelcon3d  2526  ssneld  3250  sscon  3363  difrab  3507  exmid1stab  4343  eunex  4706  ndmfvg  5724  suppssrst  6495  suppssrgst  6496  nnaord  6776  nnmord  6784  php5  7153  php5dom  7158  fidcen  7197  supmoti  7327  exmidomniim  7475  mkvprop  7492  enmkvlem  7495  prubl  7847  letr  8402  eqord1  8805  prodge0  9178  lt2msq  9210  nnge1  9310  nzadd  9680  irradd  10029  irrmul  10030  xrletr  10193  frec2uzf1od  10826  zesq  11079  expcanlem  11136  nn0opthd  11143  bccmpl  11175  fundm2domnop0  11283  maxleast  11962  fisumss  12142  dvdsbnd  12716  prm2orodd  12887  coprm  12905  prmndvdsfaclt  12917  hashgcdeq  13001  ballotfilemfc0  13215  ballotfilemfcc  13216  cos11  15937  bj-nnsn  16744  bj-nnelirr  16962  ismkvnnlem  17076  nconstwlpolem  17089