Theorem con3d 631

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3rr3  633  con3dimp  635  con3  642  nsyld  648  nsyli  649  jcn  651  notbi  666  impidc  858  bijadc  882  pm2.13dc  885  xoranor  1377  mo2n  2054  necon3ad  2389  necon3bd  2390  nelcon3d  2453  ssneld  3157  sscon  3269  difrab  3409  exmid1stab  4208  eunex  4560  ndmfvg  5546  nnaord  6509  nnmord  6517  php5  6857  php5dom  6862  supmoti  6991  exmidomniim  7138  mkvprop  7155  enmkvlem  7158  prubl  7484  letr  8039  eqord1  8439  prodge0  8810  lt2msq  8842  nnge1  8941  nzadd  9304  irradd  9645  irrmul  9646  xrletr  9807  frec2uzf1od  10405  zesq  10638  expcanlem  10694  nn0opthd  10701  bccmpl  10733  maxleast  11221  fisumss  11399  dvdsbnd  11956  prm2orodd  12125  coprm  12143  prmndvdsfaclt  12155  hashgcdeq  12238  cos11  14244  bj-nnsn  14455  bj-nnelirr  14675  ismkvnnlem  14770  nconstwlpolem  14782