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 36144

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 492	. . 3 $/\$ $\/$
2		anor 492	. . 3 $/\$ $\/$
3		ifpbi23 36110	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ if- $/\$ $/\$ if- $\/$ $\/$
4	1, 2, 3	mp2an 677	. 2 if- $/\$ $/\$ if- $\/$ $\/$
5		ifpororb 36143	. . . . 5 if- $\/$ $\/$ if- $\/$ if-
6		ifpnotnotb 36117	. . . . . 6 if- if-
7		ifpnotnotb 36117	. . . . . 6 if- if-
8	6, 7	orbi12i 524	. . . . 5 if- $\/$ if- if- $\/$ if-
9	5, 8	bitri 253	. . . 4 if- $\/$ $\/$ if- $\/$ if-
10	9	notbii 298	. . 3 if- $\/$ $\/$ if- $\/$ if-
11		ifpnotnotb 36117	. . 3 if- $\/$ $\/$ if- $\/$ $\/$
12		anor 492	. . 3 if- $/\$ if- if- $\/$ if-
13	10, 11, 12	3bitr4i 281	. 2 if- $\/$ $\/$ if- $/\$ if-
14	4, 13	bitri 253	1 if- $/\$ $/\$ if- $/\$ if-

Colors of variables: wff setvar class

Syntax hints:

wn 3

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

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 1425

This theorem is referenced by: ifpnannanb 36145