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

Theorem con3d 594
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 592 . . 3 (𝜒 → ¬ ¬ 𝜒)
31, 2syl6 33 . 2 (𝜑 → (𝜓 → ¬ ¬ 𝜒))
43con2d 587 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 577  ax-in2 578
This theorem is referenced by:  con3rr3  596  con3dimp  597  con3  604  nsyld  610  nsyli  611  mth8  612  notbid  625  impidc  791  bijadc  812  pm2.13dc  815  xoranor  1311  mo2n  1973  necon3ad  2293  necon3bd  2294  ssneld  3016  sscon  3123  difrab  3262  eunex  4349  ndmfvg  5292  nnaord  6214  nnmord  6222  php5  6520  php5dom  6525  supmoti  6625  exmidomniim  6734  prubl  6982  letr  7505  prodge0  8243  lt2msq  8275  nnge1  8373  nzadd  8728  irradd  9056  irrmul  9057  xrletr  9198  frec2uzf1od  9734  zesq  9961  expcanlem  10013  nn0opthd  10019  bccmpl  10051  maxleast  10534  dvdsbnd  10815  prm2orodd  10975  coprm  10990  prmndvdsfaclt  11002  hashgcdeq  11071  bj-notbi  11246  bj-nnelirr  11278
  Copyright terms: Public domain W3C validator