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  3227  sscon  3339  difrab  3479  exmid1stab  4296  eunex  4657  ndmfvg  5666  nnaord  6672  nnmord  6680  php5  7039  php5dom  7044  fidcen  7083  supmoti  7186  exmidomniim  7334  mkvprop  7351  enmkvlem  7354  prubl  7699  letr  8255  eqord1  8656  prodge0  9027  lt2msq  9059  nnge1  9159  nzadd  9525  irradd  9873  irrmul  9874  xrletr  10036  frec2uzf1od  10661  zesq  10913  expcanlem  10970  nn0opthd  10977  bccmpl  11009  fundm2domnop0  11102  maxleast  11767  fisumss  11946  dvdsbnd  12520  prm2orodd  12691  coprm  12709  prmndvdsfaclt  12721  hashgcdeq  12805  cos11  15570  bj-nnsn  16279  bj-nnelirr  16498  ismkvnnlem  16606  nconstwlpolem  16619