ifpim23g - Mathbox for Richard Penner

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

Theorem ifpim23g 37840

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

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

**Proof of Theorem ifpim23g**
Step	Hyp	Ref	Expression
1		ifpidg 37836	. 2 if- $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
2		dfor2 427	. . . . 5 $\/$
3	2	imbi2i 326	. . . 4 $\/$
4		impexp 462	. . . 4 $/\$
5		ax-1 6	. . . . . 6
6	5	adantl 482	. . . . 5 $/\$
7	6	biantrur 527	. . . 4 $/\$ $/\$ $/\$ $/\$
8	3, 4, 7	3bitr2i 288	. . 3 $\/$ $/\$ $/\$ $/\$
9		impexp 462	. . . . 5 $/\$
10		imdi 378	. . . . . 6
11		imor 428	. . . . . . . 8 $\/$
12		orcom 402	. . . . . . . 8 $\/$ $\/$
13	11, 12	bitri 264	. . . . . . 7 $\/$
14	13	imbi2i 326	. . . . . 6 $\/$
15	10, 14	bitri 264	. . . . 5 $\/$
16	9, 15	bitri 264	. . . 4 $/\$ $\/$
17		pm2.21 120	. . . . . 6
18	17	olcd 408	. . . . 5 $\/$
19	18	biantrur 527	. . . 4 $\/$ $\/$ $/\$ $\/$
20	16, 19	bitri 264	. . 3 $/\$ $\/$ $/\$ $\/$
21	8, 20	anbi12i 733	. 2 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
22		ancom 466	. 2 $\/$ $/\$ $/\$ $/\$ $/\$ $\/$
23	1, 21, 22	3bitr2i 288	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: ifpim3 37841 ifpim4 37843