hbn1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > hbn1		Structured version Visualization version Unicode version

Theorem hbn1 1926

Description: Alias for ax-10 1925 to be used instead of it. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.)

**Assertion**
Ref	Expression
hbn1

**Proof of Theorem hbn1**
Step	Hyp	Ref	Expression
1		ax-10 1925	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wal 1452

This theorem was proved from axioms: ax-10 1925

This theorem is referenced by: hbe1 1927 modal-5 1929 axc4 1948 axc7 1949 axc14 2211 bj-modal5e 31293 ax12indn 32558 axc5c4c711 36795 vk15.4j 36928 ax6e2nd 36968 ax6e2ndVD 37344 ax6e2ndALT 37366