Theorem con3d 632

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3rr3  634  con3dimp  636  con3  643  nsyld  649  nsyli  650  jcn  652  notbi  667  impidc  859  bijadc  883  pm2.13dc  886  xoranor  1388  mo2n  2073  necon3ad  2409  necon3bd  2410  nelcon3d  2473  ssneld  3186  sscon  3298  difrab  3438  exmid1stab  4242  eunex  4598  ndmfvg  5592  nnaord  6576  nnmord  6584  php5  6928  php5dom  6933  supmoti  7068  exmidomniim  7216  mkvprop  7233  enmkvlem  7236  prubl  7572  letr  8128  eqord1  8529  prodge0  8900  lt2msq  8932  nnge1  9032  nzadd  9397  irradd  9739  irrmul  9740  xrletr  9902  frec2uzf1od  10517  zesq  10769  expcanlem  10826  nn0opthd  10833  bccmpl  10865  maxleast  11397  fisumss  11576  dvdsbnd  12150  prm2orodd  12321  coprm  12339  prmndvdsfaclt  12351  hashgcdeq  12435  cos11  15175  bj-nnsn  15465  bj-nnelirr  15685  ismkvnnlem  15787  nconstwlpolem  15800