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

Theorem con3i 549
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 546 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 532  ax-in2 533
This theorem is referenced by:  pm2.51  568  pm5.21ni  606  notnotnot  615  pm2.45  644  pm2.46  645  pm3.14  657  3ianorr  1189  nalequcoms  1391  equidqe  1406  equidqeOLD  1407  ax6blem  1522  hbnt  1525  naecoms  1594  euor2  1940  moexexdc  1966  baroco  1989  necon3ai  2232  necon3bi  2233  eueq3dc  2692  difin  3151  indifdir  3170  difrab  3188  csbprc  3239  nelpri  3371  opprc  3544  opprc1  3545  opprc2  3546  eldifpw  4158  nlimsucg  4226  nfvres  5131  nfunsn  5132  ressnop0  5269  ovprc  5463  ovprc1  5464  ovprc2  5465
  Copyright terms: Public domain W3C validator