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

Theorem con3d 561
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 notnot 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  563  con3and  564  con3  571  nsyld  577  nsyli  578  mth8  579  notbid  592  impidc  755  bijadc  776  pm2.13dc  779  xoranor  1268  mo2n  1928  necon3ad  2244  necon3bd  2245  ssneld  2944  sscon  3074  difrab  3208  eunex  4270  ndmfvg  5182  nnaord  6060  nnmord  6068  php5  6299  php5dom  6303  prubl  6556  letr  7072  prodge0  7787  lt2msq  7819  nnge1  7904  irradd  8542  irrmul  8543  xrletr  8682  frec2uzf1od  9061  zesq  9236  bj-notbi  9909  bj-nnelirr  9942
  Copyright terms: Public domain W3C validator