ifpororb - Mathbox for Richard Penner

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

Theorem ifpororb 37850

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

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

**Proof of Theorem ifpororb**
Step	Hyp	Ref	Expression
1		dfifp2 1014	. 2 if- $\/$ $\/$ $\/$ $/\$ $\/$
2		df-or 385	. . . 4 $\/$
3	2	imbi2i 326	. . 3 $\/$
4		df-or 385	. . . 4 $\/$
5	4	imbi2i 326	. . 3 $\/$
6	3, 5	anbi12i 733	. 2 $\/$ $/\$ $\/$ $/\$
7		ifpimimb 37849	. . 3 if- if- if-
8		dfifp2 1014	. . 3 if- $/\$
9		imor 428	. . . 4 if- if- if- $\/$ if-
10		ifpnot23d 37830	. . . . 5 if- if-
11	10	orbi1i 542	. . . 4 if- $\/$ if- if- $\/$ if-
12	9, 11	bitri 264	. . 3 if- if- if- $\/$ if-
13	7, 8, 12	3bitr3i 290	. 2 $/\$ if- $\/$ if-
14	1, 6, 13	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: ifpananb 37851