axc5c7toc7 - Mathbox for Norm Megill

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

Theorem axc5c7toc7 34198

Description: Rederivation of ax-c7 34170 from axc5c7 34196. Only propositional calculus is used for the rederivation. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.)

**Assertion**
Ref	Expression
axc5c7toc7

**Proof of Theorem axc5c7toc7**
Step	Hyp	Ref	Expression
1		pm2.21 120	. 2
2		axc5c7 34196	. 2
3	1, 2	syl 17	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-c5 34168 ax-c7 34170

This theorem is referenced by: (None)

W3C validator