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

Theorem con3i 561
Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)
Hypothesis
Ref Expression
con3i.a (φψ)
Assertion
Ref Expression
con3i ψ → ¬ φ)

Proof of Theorem con3i
StepHypRef Expression
1 id 19 . 2 ψ → ¬ ψ)
2 con3i.a . 2 (φψ)
31, 2nsyl 558 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:  pm2.51  580  pm5.21ni  618  notnotnot  627  pm2.45  656  pm2.46  657  pm3.14  669  3ianorr  1203  nalequcoms  1407  equidqe  1422  ax6blem  1537  hbnt  1540  naecoms  1609  euor2  1955  moexexdc  1981  baroco  2004  necon3ai  2248  necon3bi  2249  eueq3dc  2709  difin  3168  indifdir  3187  difrab  3205  csbprc  3256  nelpri  3388  opprc  3561  opprc1  3562  opprc2  3563  eldifpw  4174  nlimsucg  4242  nfvres  5149  nfunsn  5150  ressnop0  5287  ovprc  5482  ovprc1  5483  ovprc2  5484  fiprc  6228  fzdcel  8674
  Copyright terms: Public domain W3C validator