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  862  bijadc  886  pm2.13dc  889  xoranor  1399  mo2n  2085  necon3ad  2422  necon3bd  2423  nelcon3d  2486  ssneld  3206  sscon  3318  difrab  3458  exmid1stab  4271  eunex  4630  ndmfvg  5634  nnaord  6625  nnmord  6633  php5  6987  php5dom  6992  supmoti  7128  exmidomniim  7276  mkvprop  7293  enmkvlem  7296  prubl  7641  letr  8197  eqord1  8598  prodge0  8969  lt2msq  9001  nnge1  9101  nzadd  9467  irradd  9809  irrmul  9810  xrletr  9972  frec2uzf1od  10595  zesq  10847  expcanlem  10904  nn0opthd  10911  bccmpl  10943  fundm2domnop0  11034  maxleast  11690  fisumss  11869  dvdsbnd  12443  prm2orodd  12614  coprm  12632  prmndvdsfaclt  12644  hashgcdeq  12728  cos11  15492  bj-nnsn  16007  bj-nnelirr  16226  ismkvnnlem  16331  nconstwlpolem  16344