ifpimimb - Mathbox for Richard Penner

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

Theorem ifpimimb 37849

Description: Factor conditional logic operator over implication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)

**Assertion**
Ref	Expression
ifpimimb	if- if- if-

**Proof of Theorem ifpimimb**
Step	Hyp	Ref	Expression
1		dfifp2 1014	. 2 if- $/\$
2		imor 428	. . . 4 $\/$
3		pm4.8 380	. . . . . 6
4	3	bicomi 214	. . . . 5
5	4	orbi1i 542	. . . 4 $\/$ $\/$
6		id 22	. . . . . 6
7	6	orci 405	. . . . 5 $\/$
8	7	biantru 526	. . . 4 $\/$ $\/$ $/\$ $\/$
9	2, 5, 8	3bitri 286	. . 3 $\/$ $/\$ $\/$
10		pm4.64 387	. . . 4 $\/$
11		pm4.81 381	. . . . . 6
12	11	bicomi 214	. . . . 5
13	12	orbi1i 542	. . . 4 $\/$ $\/$
14	6	orci 405	. . . . 5 $\/$
15	14	biantrur 527	. . . 4 $\/$ $\/$ $/\$ $\/$
16	10, 13, 15	3bitri 286	. . 3 $\/$ $/\$ $\/$
17	9, 16	anbi12i 733	. 2 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
18		ifpim123g 37845	. . 3 if- if- $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
19	18	bicomi 214	. 2 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ if- if-
20	1, 17, 19	3bitri 286	1 if- if- 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: ifpororb 37850 ifpbibib 37855