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

Theorem con3i 604
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 600 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 586  ax-in2 587
This theorem is referenced by:  notnotnot  606  conax1  625  pm5.21ni  675  pm2.45  710  pm2.46  711  pm3.14  725  3ianorr  1270  nalequcoms  1480  equidqe  1495  ax6blem  1611  hbnt  1614  naecoms  1685  euor2  2033  moexexdc  2059  baroco  2082  necon3ai  2331  necon3bi  2332  eueq3dc  2827  difin  3279  indifdir  3298  difrab  3316  csbprc  3374  ifandc  3474  nelpri  3517  nelprd  3519  opprc  3692  opprc1  3693  opprc2  3694  notnotsnex  4071  eldifpw  4358  nlimsucg  4441  nfvres  5408  nfunsn  5409  ressnop0  5555  ovprc  5760  ovprc1  5761  ovprc2  5762  mapprc  6500  ixpprc  6567  ixp0  6579  fiprc  6663  fidceq  6716  unfiexmid  6759  difinfsnlem  6936  fzdcel  9713  bcpasc  10405  flodddiv4lt  11481  bj-nnan  12641  bj-nnal  12642  bj-nnst  12657  nninfsellemsuc  12900
  Copyright terms: Public domain W3C validator