baihei-inj - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > baihei-inj

Theorem baihei-inj 578

Description: Inference form of ax-baihei-inj 577 (Contributed by la korvo, 30-Aug-2024.)

**Hypothesis**
Ref	Expression
baihei-inj.0	⊢ li bai'ei ku'i'a du li bai'ei ku'i'e

**Assertion**
Ref	Expression
baihei-inj	⊢ li ku'i'a du li ku'i'e

Distinct variable group: ku'i'a , ku'i'e

**Proof of Theorem baihei-inj**
Step	Hyp	Ref	Expression
1		baihei-inj.0	. 2 ⊢ li bai'ei ku'i'a du li bai'ei ku'i'e
2		ax-baihei-inj 577	. 2 ⊢ ganai li bai'ei ku'i'a du li bai'ei ku'i'e gi li ku'i'a du li ku'i'e
3	1, 2	ax-mp 10	1 ⊢ li ku'i'a du li ku'i'e

Colors of variables: sumti selbri bridi

Syntax hints: du sbdu 250 li sli 573 bai'ei mbaihei 576

This theorem was proved from axioms: ax-mp 10 ax-baihei-inj 577

This theorem is referenced by: (None)