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

Theorem con3d 626
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 624 . . 3 (𝜒 → ¬ ¬ 𝜒)
31, 2syl6 33 . 2 (𝜑 → (𝜓 → ¬ ¬ 𝜒))
43con2d 619 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 609  ax-in2 610
This theorem is referenced by:  con3rr3  628  con3dimp  630  con3  637  nsyld  643  nsyli  644  jcn  646  notbi  661  impidc  853  bijadc  877  pm2.13dc  880  xoranor  1372  mo2n  2047  necon3ad  2382  necon3bd  2383  nelcon3d  2446  ssneld  3149  sscon  3261  difrab  3401  eunex  4545  ndmfvg  5527  nnaord  6488  nnmord  6496  php5  6836  php5dom  6841  supmoti  6970  exmidomniim  7117  mkvprop  7134  enmkvlem  7137  prubl  7448  letr  8002  eqord1  8402  prodge0  8770  lt2msq  8802  nnge1  8901  nzadd  9264  irradd  9605  irrmul  9606  xrletr  9765  frec2uzf1od  10362  zesq  10594  expcanlem  10649  nn0opthd  10656  bccmpl  10688  maxleast  11177  fisumss  11355  dvdsbnd  11911  prm2orodd  12080  coprm  12098  prmndvdsfaclt  12110  hashgcdeq  12193  cos11  13568  bj-nnsn  13768  bj-nnelirr  13988  exmid1stab  14033  ismkvnnlem  14084  nconstwlpolem  14096
  Copyright terms: Public domain W3C validator