Theorem con3d 632

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3rr3  634  con3dimp  636  con3  643  nsyld  649  nsyli  650  jcn  653  notbi  668  impidc  860  bijadc  884  pm2.13dc  887  xoranor  1397  mo2n  2083  necon3ad  2419  necon3bd  2420  nelcon3d  2483  ssneld  3196  sscon  3308  difrab  3448  exmid1stab  4256  eunex  4613  ndmfvg  5614  nnaord  6602  nnmord  6610  php5  6962  php5dom  6967  supmoti  7102  exmidomniim  7250  mkvprop  7267  enmkvlem  7270  prubl  7606  letr  8162  eqord1  8563  prodge0  8934  lt2msq  8966  nnge1  9066  nzadd  9432  irradd  9774  irrmul  9775  xrletr  9937  frec2uzf1od  10558  zesq  10810  expcanlem  10867  nn0opthd  10874  bccmpl  10906  fundm2domnop0  10997  maxleast  11568  fisumss  11747  dvdsbnd  12321  prm2orodd  12492  coprm  12510  prmndvdsfaclt  12522  hashgcdeq  12606  cos11  15369  bj-nnsn  15743  bj-nnelirr  15963  ismkvnnlem  16065  nconstwlpolem  16078