Theorem con3d 621

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3rr3  623  con3dimp  625  con3  632  nsyld  638  nsyli  639  jcn  641  notbi  656  impidc  844  bijadc  868  pm2.13dc  871  xoranor  1359  mo2n  2034  necon3ad  2369  necon3bd  2370  nelcon3d  2433  ssneld  3130  sscon  3242  difrab  3382  eunex  4522  ndmfvg  5501  nnaord  6458  nnmord  6466  php5  6805  php5dom  6810  supmoti  6939  exmidomniim  7086  mkvprop  7103  enmkvlem  7106  prubl  7408  letr  7962  eqord1  8362  prodge0  8730  lt2msq  8762  nnge1  8861  nzadd  9224  irradd  9561  irrmul  9562  xrletr  9718  frec2uzf1od  10314  zesq  10545  expcanlem  10600  nn0opthd  10607  bccmpl  10639  maxleast  11124  fisumss  11300  dvdsbnd  11855  prm2orodd  12018  coprm  12034  prmndvdsfaclt  12046  hashgcdeq  12129  cos11  13244  bj-nnsn  13380  bj-nnelirr  13599  exmid1stab  13643  ismkvnnlem  13694  nconstwlpolem  13706