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

Theorem 19.8a 1405
Description: If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
19.8a

Proof of Theorem 19.8a
StepHypRef Expression
1 id 17 . . 3
2 hbe1 1314 . . . 4
3219.23 1317 . . 3
41, 3mpbir 132 . 2
54a4i 1359 1
Colors of variables: wff set class
Syntax hints:   wi 4  wal 1264  wex 1311
This theorem is referenced by:  19.23bi  1406  exim  1411  19.43  1431  hbex  1438  19.2  1440  19.9t  1442  19.9  1443  excomim  1456  19.38  1463  nexr  1472  sbequ1  1536  equs5e  1560  exdistrf  1565  sbcof2  1575  mo  2004  mo2  2011  euor2  2051  2moex  2054  2euex  2055  2moswap  2058  2exeu  2060  2mo  2061  qexmid  2095
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-ia2 98  ax-ia3 99  ax-gen 1267  ax-ie1 1312  ax-ie2 1313  ax-4 1331
This theorem depends on definitions:  df-bi 108
  Copyright terms: Public domain W3C validator