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

Theorem con3d 603
 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 601 . . 3 (𝜒 → ¬ ¬ 𝜒)
31, 2syl6 33 . 2 (𝜑 → (𝜓 → ¬ ¬ 𝜒))
43con2d 596 1 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 586  ax-in2 587 This theorem is referenced by:  con3rr3  605  con3dimp  607  con3  614  nsyld  620  nsyli  621  mth8  622  notbi  638  impidc  826  bijadc  850  pm2.13dc  853  xoranor  1338  mo2n  2003  necon3ad  2325  necon3bd  2326  nelcon3d  2389  ssneld  3067  sscon  3178  difrab  3318  eunex  4444  ndmfvg  5418  nnaord  6371  nnmord  6379  php5  6718  php5dom  6723  supmoti  6846  exmidomniim  6979  mkvprop  6998  prubl  7258  letr  7811  eqord1  8209  cnstab  8369  prodge0  8569  lt2msq  8601  nnge1  8700  nzadd  9057  irradd  9387  irrmul  9388  xrletr  9531  frec2uzf1od  10119  zesq  10350  expcanlem  10402  nn0opthd  10408  bccmpl  10440  maxleast  10925  fisumss  11101  efler  11304  dvdsbnd  11541  prm2orodd  11703  coprm  11718  prmndvdsfaclt  11730  hashgcdeq  11799  bj-nnsn  12747  bj-nnelirr  12953  exmid1stab  12997
 Copyright terms: Public domain W3C validator