Theorem con3d 636

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3rr3  638  con3dimp  640  con3  647  nsyld  653  nsyli  654  jcn  657  notbi  672  impidc  865  bijadc  889  pm2.13dc  892  xoranor  1421  mo2n  2107  necon3ad  2444  necon3bd  2445  nelcon3d  2508  ssneld  3229  sscon  3341  difrab  3481  exmid1stab  4298  eunex  4659  ndmfvg  5670  nnaord  6677  nnmord  6685  php5  7044  php5dom  7049  fidcen  7088  supmoti  7192  exmidomniim  7340  mkvprop  7357  enmkvlem  7360  prubl  7706  letr  8262  eqord1  8663  prodge0  9034  lt2msq  9066  nnge1  9166  nzadd  9532  irradd  9880  irrmul  9881  xrletr  10043  frec2uzf1od  10669  zesq  10921  expcanlem  10978  nn0opthd  10985  bccmpl  11017  fundm2domnop0  11110  maxleast  11775  fisumss  11955  dvdsbnd  12529  prm2orodd  12700  coprm  12718  prmndvdsfaclt  12730  hashgcdeq  12814  cos11  15580  bj-nnsn  16350  bj-nnelirr  16569  ismkvnnlem  16677  nconstwlpolem  16690