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

Theorem con3i 572
 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 568 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 554  ax-in2 555 This theorem is referenced by:  pm2.51  591  pm5.21ni  629  notnotnot  638  pm2.45  667  pm2.46  668  pm3.14  680  3ianorr  1215  nalequcoms  1426  equidqe  1441  ax6blem  1556  hbnt  1559  naecoms  1628  euor2  1974  moexexdc  2000  baroco  2023  necon3ai  2269  necon3bi  2270  eueq3dc  2738  difin  3202  indifdir  3221  difrab  3239  csbprc  3290  nelpri  3427  opprc  3598  opprc1  3599  opprc2  3600  eldifpw  4236  nlimsucg  4318  nfvres  5234  nfunsn  5235  ressnop0  5372  ovprc  5568  ovprc1  5569  ovprc2  5570  fiprc  6323  fidceq  6361  fzdcel  9006  bcpasc  9634  flodddiv4lt  10248
 Copyright terms: Public domain W3C validator