axc4i-o - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > axc4i-o		Unicode version

Theorem axc4i-o 2229

Description: Inference version of ax-c4 2215. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.)

**Hypothesis**
Ref	Expression
axc4i-o.1

**Assertion**
Ref	Expression
axc4i-o

**Proof of Theorem axc4i-o**
Step	Hyp	Ref	Expression
1		hba1-o 2228	. 2
2		axc4i-o.1	. 2
3	1, 2	alrimih 1642	1

Colors of variables: wff setvar class

Syntax hints: ->wi 4 A.wal 1393

This theorem is referenced by: hbae-o 2232 aev-o 2261 axc11n-16 2268 ax12indalem 2275 ax12inda2ALT 2276

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-c5 2214 ax-c4 2215 ax-c7 2216