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

Theorem con3d 605
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 603 . . 3 (𝜒 → ¬ ¬ 𝜒)
31, 2syl6 33 . 2 (𝜑 → (𝜓 → ¬ ¬ 𝜒))
43con2d 598 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 588  ax-in2 589
This theorem is referenced by:  con3rr3  607  con3dimp  609  con3  616  nsyld  622  nsyli  623  mth8  624  notbi  640  impidc  828  bijadc  852  pm2.13dc  855  xoranor  1340  mo2n  2005  necon3ad  2327  necon3bd  2328  nelcon3d  2391  ssneld  3069  sscon  3180  difrab  3320  eunex  4446  ndmfvg  5420  nnaord  6373  nnmord  6381  php5  6720  php5dom  6725  supmoti  6848  exmidomniim  6981  mkvprop  7000  prubl  7262  letr  7815  eqord1  8213  cnstab  8375  prodge0  8580  lt2msq  8612  nnge1  8711  nzadd  9074  irradd  9406  irrmul  9407  xrletr  9559  frec2uzf1od  10147  zesq  10378  expcanlem  10430  nn0opthd  10436  bccmpl  10468  maxleast  10953  fisumss  11129  efler  11332  dvdsbnd  11572  prm2orodd  11734  coprm  11749  prmndvdsfaclt  11761  hashgcdeq  11831  bj-nnsn  12872  bj-nnelirr  13078  exmid1stab  13122
  Copyright terms: Public domain W3C validator