ifpim1g - Mathbox for Richard Penner

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

Theorem ifpim1g 37846

Description: Implication of conditional logical operators. (Contributed by RP, 18-Apr-2020.)

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

**Proof of Theorem ifpim1g**
Step	Hyp	Ref	Expression
1		ifpim123g 37845	. 2 if- if- $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
2		id 22	. . . . . 6
3	2	olci 406	. . . . 5 $\/$
4	3	biantrur 527	. . . 4 $\/$ $\/$ $/\$ $\/$
5	4	bicomi 214	. . 3 $\/$ $/\$ $\/$ $\/$
6		id 22	. . . . . 6
7	6	olci 406	. . . . 5 $\/$
8	7	biantru 526	. . . 4 $\/$ $\/$ $/\$ $\/$
9	8	bicomi 214	. . 3 $\/$ $/\$ $\/$ $\/$
10	5, 9	anbi12i 733	. 2 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
11	1, 10	bitri 264	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: ifp1bi 37847