Theorem con3d 620

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3rr3  622  con3dimp  624  con3  631  nsyld  637  nsyli  638  jcn  640  notbi  655  impidc  843  bijadc  867  pm2.13dc  870  xoranor  1355  mo2n  2027  necon3ad  2350  necon3bd  2351  nelcon3d  2414  ssneld  3099  sscon  3210  difrab  3350  eunex  4476  ndmfvg  5452  nnaord  6405  nnmord  6413  php5  6752  php5dom  6757  supmoti  6880  exmidomniim  7013  mkvprop  7032  prubl  7294  letr  7847  eqord1  8245  cnstab  8407  prodge0  8612  lt2msq  8644  nnge1  8743  nzadd  9106  irradd  9438  irrmul  9439  xrletr  9591  frec2uzf1od  10179  zesq  10410  expcanlem  10462  nn0opthd  10468  bccmpl  10500  maxleast  10985  fisumss  11161  efler  11405  dvdsbnd  11645  prm2orodd  11807  coprm  11822  prmndvdsfaclt  11834  hashgcdeq  11904  bj-nnsn  12945  bj-nnelirr  13151  exmid1stab  13195