ifpananb - Mathbox for Richard Penner

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

Theorem ifpananb 36221

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

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

**Proof of Theorem ifpananb**
Step	Hyp	Ref	Expression
1		anor 497	. . 3 $/\$ $\/$
2		anor 497	. . 3 $/\$ $\/$
3		ifpbi23 36187	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ if- $/\$ $/\$ if- $\/$ $\/$
4	1, 2, 3	mp2an 686	. 2 if- $/\$ $/\$ if- $\/$ $\/$
5		ifpororb 36220	. . . . 5 if- $\/$ $\/$ if- $\/$ if-
6		ifpnotnotb 36194	. . . . . 6 if- if-
7		ifpnotnotb 36194	. . . . . 6 if- if-
8	6, 7	orbi12i 530	. . . . 5 if- $\/$ if- if- $\/$ if-
9	5, 8	bitri 257	. . . 4 if- $\/$ $\/$ if- $\/$ if-
10	9	notbii 303	. . 3 if- $\/$ $\/$ if- $\/$ if-
11		ifpnotnotb 36194	. . 3 if- $\/$ $\/$ if- $\/$ $\/$
12		anor 497	. . 3 if- $/\$ if- if- $\/$ if-
13	10, 11, 12	3bitr4i 285	. 2 if- $\/$ $\/$ if- $/\$ if-
14	4, 13	bitri 257	1 if- $/\$ $/\$ if- $/\$ if-

Colors of variables: wff setvar class

Syntax hints:

wn 3

wb 189 $\/$ wo 375 $/\$ wa 376 if-wif 983

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 190 df-or 377 df-an 378 df-ifp 984

This theorem is referenced by: ifpnannanb 36222