exv - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > exv

Theorem exv 417

Description: A weaker version of ax-ex 416 which requires {da} and {de} to be distinct. (Contributed by la korvo, 4-Jan-2025.)

**Assertion**
Ref	Expression
exv	⊢ su'o da zo'u da du de

Distinct variable group: da , de

**Proof of Theorem exv**
Step	Hyp	Ref	Expression
1		ax-ex 416	1 ⊢ su'o da zo'u da du de

Colors of variables: sumti selbri bridi

This theorem was proved from axioms: ax-ex 416

This theorem is referenced by: (None)