Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > axc11  Structured version Unicode version 
Description: Axiom axc11 2211 was the original version of axc11n 2212 ("n" for "new"),
before it was discovered (in May 2008) that the shorter axc11n 2212 could
replace it. It appears as Axiom scheme C11' in [Megill] p. 448 (p. 16 of
the preprint).
This axiom is obsolete and should no longer be used. It is proved above as theorem axc11 2027. (Contributed by NM, 10May1993.) (New usage is discouraged.) 
Ref  Expression 

axc11 
Step  Hyp  Ref  Expression 

1  vx  . . . 4  
2  vy  . . . 4  
3  1, 2  weq 1705  . . 3 
4  3, 1  wal 1377  . 2 
5  wph  . . . 4  
6  5, 1  wal 1377  . . 3 
7  5, 2  wal 1377  . . 3 
8  6, 7  wi 4  . 2 
9  4, 8  wi 4  1 
Colors of variables: wff setvar class 
This axiom is referenced by: aecomo 2223 hbaeo 2225 dral1o 2226 axc11nfromc11 2249 dvelimfo 2252 
Copyright terms: Public domain  W3C validator 