Theorem con3d 634

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3rr3  636  con3dimp  638  con3  645  nsyld  651  nsyli  652  jcn  655  notbi  670  impidc  863  bijadc  887  pm2.13dc  890  xoranor  1419  mo2n  2105  necon3ad  2442  necon3bd  2443  nelcon3d  2506  ssneld  3226  sscon  3338  difrab  3478  exmid1stab  4292  eunex  4653  ndmfvg  5660  nnaord  6663  nnmord  6671  php5  7027  php5dom  7032  supmoti  7168  exmidomniim  7316  mkvprop  7333  enmkvlem  7336  prubl  7681  letr  8237  eqord1  8638  prodge0  9009  lt2msq  9041  nnge1  9141  nzadd  9507  irradd  9849  irrmul  9850  xrletr  10012  frec2uzf1od  10636  zesq  10888  expcanlem  10945  nn0opthd  10952  bccmpl  10984  fundm2domnop0  11075  maxleast  11732  fisumss  11911  dvdsbnd  12485  prm2orodd  12656  coprm  12674  prmndvdsfaclt  12686  hashgcdeq  12770  cos11  15535  bj-nnsn  16121  bj-nnelirr  16340  fidcen  16379  ismkvnnlem  16450  nconstwlpolem  16463