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

Axiom ax-gen 1218
Description: Rule of Generalization. The postulated inference rule of pure predicate calculus. See e.g. Rule 2 of [Hamilton] p. 74. This rule says that if something is unconditionally true, then it is true for all values of a variable. For example, if we have proved , we can conclude or even . Theorem a4i 1295 shows we can go the other way also: in other words we can add or remove universal quantifiers from the beginning of any theorem as required. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
ax-g.1
Assertion
Ref Expression
ax-gen

Detailed syntax breakdown of Axiom ax-gen
StepHypRef Expression
1 wph . 2
2 vx . 2
31, 2wal 1214 1
Colors of variables: wff set class
This axiom is referenced by:  gen2  1219  mpg  1220  mpgbi  1221  mpgbir  1222  hbth  1234  19.23  1258  equidqeOLD  1285  ax5o  1287  ax5  1289  ax6  1292  19.9t  1367  stdpc6  1393  cbv3  1429  equveli  1435  ax4  1808  ax11eq  1810  a12lem1  1822
  Copyright terms: Public domain W3C validator