sylibrd - New Foundations Explorer

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

Theorem sylibrd 225

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

**Hypotheses**
Ref	Expression
sylibrd.1
sylibrd.2

**Assertion**
Ref	Expression
sylibrd

**Proof of Theorem sylibrd**
Step	Hyp	Ref	Expression
1		sylibrd.1	. 2
2		sylibrd.2	. . 3
3	2	biimprd 214	. 2
4	1, 3	syld 40	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 176

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

This theorem depends on definitions: df-bi 177

This theorem is referenced by: 3imtr4d 259 sbciegft 3076 eqsbc3r 3103 fconstfv 5456 nmembers1 6271 nchoicelem12 6300