baihei-inj - brismu bridi

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

Theorem baihei-inj 516

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

**Hypothesis**
Ref	Expression
baihei-inj.0	⊢ li 1+ ku'i'a du li 1+ 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 1+ ku'i'a du li 1+ ku'i'e
2		ax-baihei-inj 515	. 2 ⊢ ganai li 1+ ku'i'a du li 1+ 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 214 li sli 511 1+ mbaihei 514

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

This theorem is referenced by: (None)