ifpidg - Mathbox for Richard Penner

	Mathbox for Richard Penner		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ifpidg		Structured version Visualization version Unicode version

Theorem ifpidg 37836

Description: Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)

**Assertion**
Ref	Expression
ifpidg	if- $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$

**Proof of Theorem ifpidg**
Step	Hyp	Ref	Expression
1		dfifp4 1016	. . 3 if- $\/$ $/\$ $\/$
2	1	bibi2i 327	. 2 if- $\/$ $/\$ $\/$
3		dfbi2 660	. . 3 $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
4		imor 428	. . . . 5 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$
5		ordi 908	. . . . 5 $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$
6		ancomst 468	. . . . . . 7 $/\$ $/\$
7		impexp 462	. . . . . . 7 $/\$
8		imor 428	. . . . . . . . 9 $\/$
9	8	imbi2i 326	. . . . . . . 8 $\/$
10		imor 428	. . . . . . . 8 $\/$ $\/$ $\/$
11	9, 10	bitri 264	. . . . . . 7 $\/$ $\/$
12	6, 7, 11	3bitrri 287	. . . . . 6 $\/$ $\/$ $/\$
13		imor 428	. . . . . . 7 $\/$ $\/$ $\/$
14	13	bicomi 214	. . . . . 6 $\/$ $\/$ $\/$
15	12, 14	anbi12i 733	. . . . 5 $\/$ $\/$ $/\$ $\/$ $\/$ $/\$ $/\$ $\/$
16	4, 5, 15	3bitri 286	. . . 4 $\/$ $/\$ $\/$ $/\$ $/\$ $\/$
17	8	bicomi 214	. . . . . . . 8 $\/$
18		df-or 385	. . . . . . . 8 $\/$
19	17, 18	anbi12i 733	. . . . . . 7 $\/$ $/\$ $\/$ $/\$
20		cases2 993	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$
21	20	bicomi 214	. . . . . . 7 $/\$ $/\$ $\/$ $/\$
22	19, 21	bitri 264	. . . . . 6 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
23	22	imbi1i 339	. . . . 5 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
24		jaob 822	. . . . 5 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
25		ancomst 468	. . . . . . 7 $/\$ $/\$
26		pm5.6 951	. . . . . . 7 $/\$ $\/$
27	25, 26	bitri 264	. . . . . 6 $/\$ $\/$
28	27	anbi2i 730	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
29	23, 24, 28	3bitri 286	. . . 4 $\/$ $/\$ $\/$ $/\$ $/\$ $\/$
30	16, 29	anbi12i 733	. . 3 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
31	3, 30	bitri 264	. 2 $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
32		ancom 466	. . 3 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$
33		an4 865	. . 3 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
34	32, 33	bitri 264	. 2 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
35	2, 31, 34	3bitri 286	1 if- $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 if-wif 1012

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 df-or 385 df-an 386 df-ifp 1013

This theorem is referenced by: ifpid3g 37837 ifpid2g 37838 ifpid1g 37839 ifpim23g 37840

W3C validator