Theorem con3d 561

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3rr3  563  con3and  564  con3  571  nsyld  577  nsyli  578  mth8  579  notbid  592  impidc  755  bijadc  776  pm2.13dc  779  xoranor  1268  mo2n  1928  necon3ad  2247  necon3bd  2248  ssneld  2947  sscon  3077  difrab  3211  eunex  4285  ndmfvg  5204  nnaord  6082  nnmord  6090  php5  6321  php5dom  6325  prubl  6584  letr  7101  prodge0  7820  lt2msq  7852  nnge1  7937  irradd  8580  irrmul  8581  xrletr  8724  frec2uzf1od  9192  zesq  9367  bj-notbi  10045  bj-nnelirr  10078