3anbi1d - New Foundations Explorer

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

Theorem 3anbi1d 1256

Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)

**Hypothesis**
Ref	Expression
3anbi1d.1

**Assertion**
Ref	Expression
3anbi1d	$/\$ $/\$ $/\$ $/\$

**Proof of Theorem 3anbi1d**
Step	Hyp	Ref	Expression
1		3anbi1d.1	. 2
2		biidd 228	. 2
3	1, 2	3anbi12d 1253	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 176 $/\$ w3a 934

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 df-an 360 df-3an 936

This theorem is referenced by: vtocl3gaf 2923 opkelins2kg 4251 opkelins3kg 4252 opkelsikg 4264 sikss1c1c 4267 brsi 4761 funsi 5520 brsnsi 5773 fnpprod 5843 ovce 6172