Theorem con3d 631

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3rr3  633  con3dimp  635  con3  642  nsyld  648  nsyli  649  jcn  651  notbi  666  impidc  858  bijadc  882  pm2.13dc  885  xoranor  1377  mo2n  2054  necon3ad  2389  necon3bd  2390  nelcon3d  2453  ssneld  3158  sscon  3270  difrab  3410  exmid1stab  4209  eunex  4561  ndmfvg  5547  nnaord  6510  nnmord  6518  php5  6858  php5dom  6863  supmoti  6992  exmidomniim  7139  mkvprop  7156  enmkvlem  7159  prubl  7485  letr  8040  eqord1  8440  prodge0  8811  lt2msq  8843  nnge1  8942  nzadd  9305  irradd  9646  irrmul  9647  xrletr  9808  frec2uzf1od  10406  zesq  10639  expcanlem  10695  nn0opthd  10702  bccmpl  10734  maxleast  11222  fisumss  11400  dvdsbnd  11957  prm2orodd  12126  coprm  12144  prmndvdsfaclt  12156  hashgcdeq  12239  cos11  14277  bj-nnsn  14488  bj-nnelirr  14708  ismkvnnlem  14803  nconstwlpolem  14815