syl56 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > syl56		Unicode version

Theorem syl56 30

Description: Combine syl5 28 and syl6 29. (Contributed by NM, 14-Nov-2013.)

**Assertion**
Ref	Expression
syl56

**Proof of Theorem syl56**
Step	Hyp	Ref	Expression
1		syl56.1	. 2
2		syl56.2	. . 3
3		syl56.3	. . 3
4	2, 3	syl6 29	. 2
5	1, 4	syl5 28	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 8

This theorem is referenced by: spfw 1691 spw 1694 dvelimhw 1849 dvelimv 1939 ax10 1944 cbv2h 1980 euind 3023 reuind 3039 cores 5084 nchoicelem9 6297 fnfrec 6320