Theorem con3d 636

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3rr3  638  con3dimp  640  con3  647  nsyld  653  nsyli  654  jcn  657  notbi  672  impidc  865  bijadc  889  pm2.13dc  892  xoranor  1421  mo2n  2106  necon3ad  2443  necon3bd  2444  nelcon3d  2507  ssneld  3228  sscon  3340  difrab  3480  exmid1stab  4300  eunex  4661  ndmfvg  5673  nnaord  6682  nnmord  6690  php5  7049  php5dom  7054  fidcen  7093  supmoti  7197  exmidomniim  7345  mkvprop  7362  enmkvlem  7365  prubl  7711  letr  8267  eqord1  8668  prodge0  9039  lt2msq  9071  nnge1  9171  nzadd  9537  irradd  9885  irrmul  9886  xrletr  10048  frec2uzf1od  10674  zesq  10926  expcanlem  10983  nn0opthd  10990  bccmpl  11022  fundm2domnop0  11118  maxleast  11796  fisumss  11976  dvdsbnd  12550  prm2orodd  12721  coprm  12739  prmndvdsfaclt  12751  hashgcdeq  12835  cos11  15606  bj-nnsn  16390  bj-nnelirr  16608  ismkvnnlem  16724  nconstwlpolem  16737