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  866  bijadc  890  pm2.13dc  893  xoranor  1422  mo2n  2108  necon3ad  2454  necon3bd  2455  nelcon3d  2518  ssneld  3239  sscon  3352  difrab  3494  exmid1stab  4320  eunex  4682  ndmfvg  5700  suppssrst  6460  suppssrgst  6461  nnaord  6741  nnmord  6749  php5  7111  php5dom  7116  fidcen  7155  supmoti  7283  exmidomniim  7431  mkvprop  7448  enmkvlem  7451  prubl  7797  letr  8352  eqord1  8753  prodge0  9124  lt2msq  9156  nnge1  9256  nzadd  9626  irradd  9974  irrmul  9975  xrletr  10137  frec2uzf1od  10764  zesq  11016  expcanlem  11073  nn0opthd  11080  bccmpl  11112  fundm2domnop0  11213  maxleast  11891  fisumss  12071  dvdsbnd  12645  prm2orodd  12816  coprm  12834  prmndvdsfaclt  12846  hashgcdeq  12930  cos11  15705  bj-nnsn  16492  bj-nnelirr  16710  ismkvnnlem  16824  nconstwlpolem  16837