Theorem con3d 594

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3rr3  596  con3dimp  597  con3  604  nsyld  610  nsyli  611  mth8  612  notbid  625  impidc  789  bijadc  810  pm2.13dc  813  xoranor  1309  mo2n  1970  necon3ad  2288  necon3bd  2289  ssneld  3002  sscon  3107  difrab  3239  eunex  4306  ndmfvg  5230  nnaord  6141  nnmord  6149  php5  6383  php5dom  6388  supmoti  6455  prubl  6727  letr  7250  prodge0  7988  lt2msq  8020  nnge1  8118  nzadd  8473  irradd  8801  irrmul  8802  xrletr  8943  frec2uzf1od  9477  zesq  9677  expcanlem  9729  nn0opthd  9735  bccmpl  9767  maxleast  10226  dvdsbnd  10481  prm2orodd  10641  coprm  10656  prmndvdsfaclt  10668  bj-notbi  10859  bj-nnelirr  10891