brismu bridi		< Previous   Next > Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  mp-ceihi

---

Theorem mp-ceihi 233

Description: A proposition implied by {cei'i} is always true. (Contributed by la korvo, 4-Jan-2025.)

Hypothesis

Ref	Expression
mp-ceihi.0	⊢ ganai cei'i gi broda

Assertion

Ref	Expression
mp-ceihi	⊢ broda

---

Proof of Theorem mp-ceihi

Step	Hyp	Ref	Expression
1		ceihi 232	. 2 ⊢ cei'i
2		mp-ceihi.0	. 2 ⊢ ganai cei'i gi broda
3	1, 2	ax-mp 10	1 ⊢ broda

Colors of variables: sumti selbri bridi

Syntax hints:  cei'i bceihi 230

This theorem was proved from axioms:  ax-mp 10  ax-k 11  ax-s 15  ax-ge-le 43  ax-ge-re 44  ax-ge-in 45  ax-gen2 195  ax-qi2 204

This theorem depends on definitions:  df-go 61  df-o 167  df-du 215  df-ceihi 231

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator