cliftetb - Mathbox for Jarvin Udandy

	Mathbox for Jarvin Udandy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cliftetb		Structured version Visualization version Unicode version

Theorem cliftetb 41105

Description: show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)

**Hypotheses**
Ref	Expression
cliftetb.1	$/\$ $\/$ $/\$
cliftetb.2

**Assertion**
Ref	Expression
cliftetb	$/\$ $\/$ $/\$

**Proof of Theorem cliftetb**
Step	Hyp	Ref	Expression
1		cliftetb.2	. 2
2		cliftetb.1	. 2 $/\$ $\/$ $/\$
3	1, 2	2th 254	1 $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wb 196 $\/$ wo 383 $/\$ wa 384

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8

This theorem depends on definitions: df-bi 197

This theorem is referenced by: (None)