axc711toc7 - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > axc711toc7		Structured version Visualization version Unicode version

Theorem axc711toc7 34201

Description: Rederivation of ax-c7 34170 from axc711 34199. Note that ax-c7 34170 and ax-11 2034 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)

**Assertion**
Ref	Expression
axc711toc7

**Proof of Theorem axc711toc7**
Step	Hyp	Ref	Expression
1		hba1-o 34182	. . . . 5
2	1	con3i 150	. . . 4
3	2	alimi 1739	. . 3
4	3	con3i 150	. 2
5		axc711 34199	. 2
6		ax-c5 34168	. 2
7	4, 5, 6	3syl 18	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wal 1481

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-11 2034 ax-c5 34168 ax-c4 34169 ax-c7 34170

This theorem is referenced by: axc711to11 34202

W3C validator