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

Theorem con3i 622
 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 618 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 604  ax-in2 605 This theorem is referenced by:  notnotnot  624  conax1  643  pm5.21ni  693  pm2.45  728  pm2.46  729  pm3.14  743  3ianorr  1288  nalequcoms  1498  equidqe  1513  ax6blem  1629  hbnt  1632  naecoms  1703  euor2  2058  moexexdc  2084  baroco  2107  necon3ai  2358  necon3bi  2359  nnral  2429  eueq3dc  2863  difin  3319  indifdir  3338  difrab  3356  csbprc  3414  ifandc  3514  nelpri  3557  nelprd  3559  opprc  3735  opprc1  3736  opprc2  3737  notnotsnex  4120  eldifpw  4407  nlimsucg  4490  nfvres  5463  nfunsn  5464  ressnop0  5610  ovprc  5815  ovprc1  5816  ovprc2  5817  mapprc  6555  ixpprc  6622  ixp0  6634  fiprc  6718  fidceq  6772  unfiexmid  6816  difinfsnlem  6994  3nsssucpw1  7107  onntri51  7110  onntri52  7113  fzdcel  9871  bcpasc  10564  flodddiv4lt  11689  bj-nnan  13139  bj-nnal  13140  bj-nnst  13155  nninfsellemsuc  13402
 Copyright terms: Public domain W3C validator