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 37851

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 510	. . 3 $/\$ $\/$
2		anor 510	. . 3 $/\$ $\/$
3		ifpbi23 37817	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ if- $/\$ $/\$ if- $\/$ $\/$
4	1, 2, 3	mp2an 708	. 2 if- $/\$ $/\$ if- $\/$ $\/$
5		ifpororb 37850	. . . . 5 if- $\/$ $\/$ if- $\/$ if-
6		ifpnotnotb 37824	. . . . . 6 if- if-
7		ifpnotnotb 37824	. . . . . 6 if- if-
8	6, 7	orbi12i 543	. . . . 5 if- $\/$ if- if- $\/$ if-
9	5, 8	bitri 264	. . . 4 if- $\/$ $\/$ if- $\/$ if-
10	9	notbii 310	. . 3 if- $\/$ $\/$ if- $\/$ if-
11		ifpnotnotb 37824	. . 3 if- $\/$ $\/$ if- $\/$ $\/$
12		anor 510	. . 3 if- $/\$ if- if- $\/$ if-
13	10, 11, 12	3bitr4i 292	. 2 if- $\/$ $\/$ if- $/\$ if-
14	4, 13	bitri 264	1 if- $/\$ $/\$ if- $/\$ if-

Colors of variables: wff setvar class

Syntax hints:

wn 3

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: ifpnannanb 37852