Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > ax10o  Structured version Unicode version 
Description: Axiom ax10o 1601 ("o" for "old") was the
original version of ax10 1393,
before it was discovered (in May 2008) that the shorter ax10 1393 could
replace it. It appears as Axiom scheme C11' in [Megill] p. 448 (p. 16 of
the preprint).
This axiom is redundant, as shown by theorem ax10o 1600. Normally, ax10o 1600 should be used rather than ax10o 1601, except by theorems specifically studying the latter's properties. (Contributed by NM, 5Aug1993.) (New usage is discouraged.) 
Ref  Expression 

ax10o 
Step  Hyp  Ref  Expression 

1  vx  . . . 4  
2  vy  . . . 4  
3  1, 2  weq 1389  . . 3 
4  3, 1  wal 1240  . 2 
5  wph  . . . 4  
6  5, 1  wal 1240  . . 3 
7  5, 2  wal 1240  . . 3 
8  6, 7  wi 4  . 2 
9  4, 8  wi 4  1 
Colors of variables: wff set class 
This axiom is referenced by: ax10 1602 
Copyright terms: Public domain  W3C validator 