ifpor123g - Mathbox for Richard Penner

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

Theorem ifpor123g 36164

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 372	. . . 4 if- $\/$ if- if- if-
2		ifpnot23 36134	. . . . 5 if- if-
3	2	imbi1i 327	. . . 4 if- if- if- if-
4	1, 3	bitri 253	. . 3 if- $\/$ if- if- if-
5		ifpim123g 36156	. . 3 if- if- $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
6	4, 5	bitri 253	. 2 if- $\/$ if- $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
7		pm4.64 374	. . . . 5 $\/$
8	7	orbi2i 522	. . . 4 $\/$ $\/$ $\/$
9		pm4.64 374	. . . . 5 $\/$
10	9	orbi2i 522	. . . 4 $\/$ $\/$ $\/$
11	8, 10	anbi12i 704	. . 3 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$
12		pm4.64 374	. . . . 5 $\/$
13	12	orbi2i 522	. . . 4 $\/$ $\/$ $\/$
14		pm4.64 374	. . . . 5 $\/$
15	14	orbi2i 522	. . . 4 $\/$ $\/$ $\/$
16	13, 15	anbi12i 704	. . 3 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$
17	11, 16	anbi12i 704	. 2 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$
18	6, 17	bitri 253	1 if- $\/$ if- $\/$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 if-wif 1427

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 189 df-or 372 df-an 373 df-ifp 1428

This theorem is referenced by: (None)