ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  con3d Structured version   GIF version

Theorem con3d 548
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
StepHypRef Expression
1 con3d.1 . . 3 (φ → (ψχ))
2 notnot1 547 . . 3 (χ → ¬ ¬ χ)
31, 2syl6 29 . 2 (φ → (ψ → ¬ ¬ χ))
43con2d 542 1 (φ → (¬ χ → ¬ ψ))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 532  ax-in2 533
This theorem is referenced by:  con3rr3  550  con3and  551  con3  558  nsyld  564  nsyli  565  mth8  566  notbid  579  impidc  743  bijadc  764  pm2.13dc  767  xoranor  1251  mo2n  1906  necon3ad  2221  necon3bd  2222  ssneld  2920  sscon  3050  difrab  3184  eunex  4219  ndmfvg  5125  nnaord  5989  nnmord  5997  prubl  6334  letr  6693  bj-nnelirr  7314
  Copyright terms: Public domain W3C validator