ifpor123g - Mathbox for Richard Penner

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

Theorem ifpor123g 36072

Description: Disjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.)

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

**Proof of Theorem ifpor123g**
Step	Hyp	Ref	Expression
1		df-or 371	. . . 4 if- $\/$ if- if- if-
2		ifpnot23 36042	. . . . 5 if- if-
3	2	imbi1i 326	. . . 4 if- if- if- if-
4	1, 3	bitri 252	. . 3 if- $\/$ if- if- if-
5		ifpim123g 36064	. . 3 if- if- $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
6	4, 5	bitri 252	. 2 if- $\/$ if- $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
7		pm4.64 373	. . . . 5 $\/$
8	7	orbi2i 521	. . . 4 $\/$ $\/$ $\/$
9		pm4.64 373	. . . . 5 $\/$
10	9	orbi2i 521	. . . 4 $\/$ $\/$ $\/$
11	8, 10	anbi12i 701	. . 3 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$
12		pm4.64 373	. . . . 5 $\/$
13	12	orbi2i 521	. . . 4 $\/$ $\/$ $\/$
14		pm4.64 373	. . . . 5 $\/$
15	14	orbi2i 521	. . . 4 $\/$ $\/$ $\/$
16	13, 15	anbi12i 701	. . 3 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$
17	11, 16	anbi12i 701	. 2 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$
18	6, 17	bitri 252	1 if- $\/$ if- $\/$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370 if-wif 1420

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 188 df-or 371 df-an 372 df-ifp 1421

This theorem is referenced by: (None)