ifpbi1b - Mathbox for Richard Penner

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

Theorem ifpbi1b 37848

Description: When the first variable is irrelevant, it can be replaced. (Contributed by RP, 25-Apr-2020.)

**Assertion**
Ref	Expression
ifpbi1b	if- if-

**Proof of Theorem ifpbi1b**
Step	Hyp	Ref	Expression
1		id 22	. . . . 5
2	1	olci 406	. . . 4 $\/$
3	1	olci 406	. . . 4 $\/$
4	2, 3	pm3.2i 471	. . 3 $\/$ $/\$ $\/$
5	1	olci 406	. . . 4 $\/$
6	1	olci 406	. . . 4 $\/$
7	5, 6	pm3.2i 471	. . 3 $\/$ $/\$ $\/$
8		ifpim123g 37845	. . 3 if- if- $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
9	4, 7, 8	mpbir2an 955	. 2 if- if-
10	1	olci 406	. . . 4 $\/$
11	10, 5	pm3.2i 471	. . 3 $\/$ $/\$ $\/$
12	1	olci 406	. . . 4 $\/$
13	3, 12	pm3.2i 471	. . 3 $\/$ $/\$ $\/$
14		ifpim123g 37845	. . 3 if- if- $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
15	11, 13, 14	mpbir2an 955	. 2 if- if-
16	9, 15	impbii 199	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)