Theorem con3d 640

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is used by:  con3rr3  642  con3dimp  644  con3  651  nsyld  657  nsyli  658  jcn  661  notbi  676  impidc  870  bijadc  894  pm2.13dc  897  xoranor  1426  mo2n  2114  necon3ad  2462  necon3bd  2463  nelcon3d  2526  ssneld  3250  sscon  3363  difrab  3507  exmid1stab  4347  eunex  4710  ndmfvg  5729  suppssrst  6505  suppssrgst  6506  nnaord  6786  nnmord  6794  php5  7164  php5dom  7169  fidcen  7208  supmoti  7340  exmidomniim  7488  mkvprop  7505  enmkvlem  7508  prubl  7860  letr  8415  eqord1  8819  prodge0  9193  lt2msq  9225  nnge1  9337  nzadd  9709  irradd  10063  irrmul  10065  xrletr  10228  frec2uzf1od  10865  zesq  11118  expcanlem  11176  nn0opthd  11183  bccmpl  11215  fundm2domnop0  11323  maxleast  12003  fisumss  12185  dvdsbnd  12759  prm2orodd  12930  coprm  12949  prmndvdsfaclt  12961  nn0sqdcq  13014  hashgcdeq  13048  ballotfilemfc0  13291  ballotfilemfcc  13292  cos11  16093  logdivlt  16136  bposlem3  16325  bj-nnsn  16978  bj-nnelirr  17196  ismkvnnlem  17321  nconstwlpolem  17334