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  4293  eunex  4654  ndmfvg  5663  nnaord  6668  nnmord  6676  php5  7032  php5dom  7037  fidcen  7074  supmoti  7176  exmidomniim  7324  mkvprop  7341  enmkvlem  7344  prubl  7689  letr  8245  eqord1  8646  prodge0  9017  lt2msq  9049  nnge1  9149  nzadd  9515  irradd  9858  irrmul  9859  xrletr  10021  frec2uzf1od  10645  zesq  10897  expcanlem  10954  nn0opthd  10961  bccmpl  10993  fundm2domnop0  11085  maxleast  11745  fisumss  11924  dvdsbnd  12498  prm2orodd  12669  coprm  12687  prmndvdsfaclt  12699  hashgcdeq  12783  cos11  15548  bj-nnsn  16206  bj-nnelirr  16425  ismkvnnlem  16534  nconstwlpolem  16547