Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > stdpc5  Structured version Unicode version 
Description: An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis can be thought of as emulating " is not free in ." With this definition, the meaning of "not free" is less restrictive than the usual textbook definition; for example would not (for us) be free in by nfequid 1587. This theorem scheme can be proved as a metatheorem of Mendelson's axiom system, even though it is slightly stronger than his Axiom 5. (Contributed by NM, 22Sep1993.) (Revised by Mario Carneiro, 12Oct2016.) (Proof shortened by Wolf Lammen, 1Jan2018.) 
Ref  Expression 

stdpc5.1 
Ref  Expression 

stdpc5 
Step  Hyp  Ref  Expression 

1  stdpc5.1  . . 3  
2  1  19.21 1472  . 2 
3  2  biimpi 113  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wal 1240 wnf 1346 
This theorem was proved from axioms: ax1 5 ax2 6 axmp 7 axia1 99 axia2 100 axia3 101 ax5 1333 axgen 1335 ax4 1397 axial 1424 axi5r 1425 
This theorem depends on definitions: dfbi 110 dfnf 1347 
This theorem is referenced by: sbalyz 1872 ra5 2840 
Copyright terms: Public domain  W3C validator 