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  866  bijadc  890  pm2.13dc  893  xoranor  1422  mo2n  2110  necon3ad  2456  necon3bd  2457  nelcon3d  2520  ssneld  3242  sscon  3355  difrab  3497  exmid1stab  4323  eunex  4685  ndmfvg  5703  suppssrst  6463  suppssrgst  6464  nnaord  6744  nnmord  6752  php5  7114  php5dom  7119  fidcen  7158  supmoti  7286  exmidomniim  7434  mkvprop  7451  enmkvlem  7454  prubl  7806  letr  8361  eqord1  8762  prodge0  9133  lt2msq  9165  nnge1  9265  nzadd  9635  irradd  9984  irrmul  9985  xrletr  10147  frec2uzf1od  10775  zesq  11028  expcanlem  11085  nn0opthd  11092  bccmpl  11124  fundm2domnop0  11228  maxleast  11906  fisumss  12086  dvdsbnd  12660  prm2orodd  12831  coprm  12849  prmndvdsfaclt  12861  hashgcdeq  12945  ballotfilemfc0  13157  ballotfilemfcc  13158  cos11  15767  bj-nnsn  16554  bj-nnelirr  16772  ismkvnnlem  16886  nconstwlpolem  16900