Theorem con3d 593

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3rr3  595  con3dimp  596  con3  603  nsyld  609  nsyli  610  mth8  611  notbid  624  impidc  788  bijadc  809  pm2.13dc  812  xoranor  1308  mo2n  1969  necon3ad  2287  necon3bd  2288  ssneld  3001  sscon  3106  difrab  3238  eunex  4304  ndmfvg  5225  nnaord  6105  nnmord  6113  php5  6344  php5dom  6349  supmoti  6406  prubl  6676  letr  7194  prodge0  7932  lt2msq  7964  nnge1  8062  nzadd  8403  irradd  8731  irrmul  8732  xrletr  8878  frec2uzf1od  9408  zesq  9591  expcanlem  9643  nn0opthd  9649  bccmpl  9681  maxleast  10099  dvdsbnd  10348  prm2orodd  10508  coprm  10523  prmndvdsfaclt  10535  bj-notbi  10716  bj-nnelirr  10748