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 37853

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 385	. . . 4 if- $\/$ if- if- if-
2		ifpnot23 37823	. . . . 5 if- if-
3	2	imbi1i 339	. . . 4 if- if- if- if-
4	1, 3	bitri 264	. . 3 if- $\/$ if- if- if-
5		ifpim123g 37845	. . 3 if- if- $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
6	4, 5	bitri 264	. 2 if- $\/$ if- $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
7		pm4.64 387	. . . . 5 $\/$
8	7	orbi2i 541	. . . 4 $\/$ $\/$ $\/$
9		pm4.64 387	. . . . 5 $\/$
10	9	orbi2i 541	. . . 4 $\/$ $\/$ $\/$
11	8, 10	anbi12i 733	. . 3 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$
12		pm4.64 387	. . . . 5 $\/$
13	12	orbi2i 541	. . . 4 $\/$ $\/$ $\/$
14		pm4.64 387	. . . . 5 $\/$
15	14	orbi2i 541	. . . 4 $\/$ $\/$ $\/$
16	13, 15	anbi12i 733	. . 3 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$
17	11, 16	anbi12i 733	. 2 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$
18	6, 17	bitri 264	1 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: (None)