Theorem con3d 636

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3rr3  638  con3dimp  640  con3  647  nsyld  653  nsyli  654  jcn  657  notbi  672  impidc  866  bijadc  890  pm2.13dc  893  xoranor  1422  mo2n  2110  necon3ad  2456  necon3bd  2457  nelcon3d  2520  ssneld  3244  sscon  3357  difrab  3499  exmid1stab  4326  eunex  4688  ndmfvg  5706  suppssrst  6474  suppssrgst  6475  nnaord  6755  nnmord  6763  php5  7125  php5dom  7130  fidcen  7169  supmoti  7297  exmidomniim  7445  mkvprop  7462  enmkvlem  7465  prubl  7817  letr  8372  eqord1  8775  prodge0  9148  lt2msq  9180  nnge1  9280  nzadd  9650  irradd  9999  irrmul  10000  xrletr  10163  frec2uzf1od  10795  zesq  11048  expcanlem  11105  nn0opthd  11112  bccmpl  11144  fundm2domnop0  11248  maxleast  11926  fisumss  12106  dvdsbnd  12680  prm2orodd  12851  coprm  12869  prmndvdsfaclt  12881  hashgcdeq  12965  ballotfilemfc0  13179  ballotfilemfcc  13180  cos11  15847  bj-nnsn  16644  bj-nnelirr  16862  ismkvnnlem  16976  nconstwlpolem  16990