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

Theorem con3d 560
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 559 . . 3 (χ → ¬ ¬ χ)
31, 2syl6 29 . 2 (φ → (ψ → ¬ ¬ χ))
43con2d 554 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 544  ax-in2 545
This theorem is referenced by:  con3rr3  562  con3and  563  con3  570  nsyld  576  nsyli  577  mth8  578  notbid  591  impidc  754  bijadc  775  pm2.13dc  778  xoranor  1267  mo2n  1925  necon3ad  2241  necon3bd  2242  ssneld  2941  sscon  3071  difrab  3205  eunex  4239  ndmfvg  5147  nnaord  6018  nnmord  6026  prubl  6469  letr  6898  prodge0  7601  lt2msq  7633  nnge1  7718  irradd  8355  irrmul  8356  xrletr  8494  frec2uzf1od  8873  zesq  9020  bj-notbi  9380  bj-nnelirr  9413
  Copyright terms: Public domain W3C validator