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  4345  eunex  4708  ndmfvg  5726  suppssrst  6501  suppssrgst  6502  nnaord  6782  nnmord  6790  php5  7159  php5dom  7164  fidcen  7203  supmoti  7333  exmidomniim  7481  mkvprop  7498  enmkvlem  7501  prubl  7853  letr  8408  eqord1  8811  prodge0  9185  lt2msq  9217  nnge1  9328  nzadd  9699  irradd  10048  irrmul  10049  xrletr  10212  frec2uzf1od  10845  zesq  11098  expcanlem  11155  nn0opthd  11162  bccmpl  11194  fundm2domnop0  11302  maxleast  11981  fisumss  12161  dvdsbnd  12735  prm2orodd  12906  coprm  12924  prmndvdsfaclt  12936  hashgcdeq  13020  ballotfilemfc0  13234  ballotfilemfcc  13235  cos11  15957  logdivlt  15999  bj-nnsn  16773  bj-nnelirr  16991  ismkvnnlem  17114  nconstwlpolem  17127