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

Theorem alnex 1385
Description: Theorem 19.7 of [Margaris] p. 89. To read this intuitionistically, think of it as "if can be refuted for all , then it is not possible to find an for which holds" (and likewise for the converse). Comparing this with dfexdc 1387 illustrates that statements which look similar (to someone used to classical logic) can be different intuitionistically due to different placement of negations. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 1-Feb-2015.) (Revised by Mario Carneiro, 12-May-2015.)
Assertion
Ref Expression
alnex

Proof of Theorem alnex
StepHypRef Expression
1 fal 1249 . . . 4
21pm2.21i 574 . . 3
3219.23h 1384 . 2
4 dfnot 1261 . . 3
54albii 1356 . 2
6 dfnot 1261 . 2
73, 5, 63bitr4i 201 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wb 98  wal 1240   wfal 1247  wex 1378
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-5 1333  ax-gen 1335  ax-ie2 1380
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-fal 1248
This theorem is referenced by:  nex  1386  dfexdc  1387  exalim  1388  ax-9  1421  alinexa  1491  nexd  1501  alexdc  1507  19.30dc  1515  19.33b2  1517  alexnim  1536  ax6blem  1537  nf4dc  1557  nf4r  1558  mo2n  1925  disjsn  3423  snprc  3426  dm0rn0  4495  reldm0  4496  dmsn0  4731  dmsn0el  4733  iotanul  4825  imadiflem  4921  imadif  4922  ltexprlemdisj  6578  recexprlemdisj  6600  fzo0  8754
  Copyright terms: Public domain W3C validator