ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  con3d Structured version   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  6468  letr  6878  prodge0  7581  lt2msq  7613  nnge1  7698  irradd  8335  irrmul  8336  xrletr  8474  frec2uzf1od  8853  zesq  9000  bj-notbi  9356  bj-nnelirr  9387
  Copyright terms: Public domain W3C validator