ifpim123g - Mathbox for Richard Penner

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

Theorem ifpim123g 37845

Description: Implication of conditional logical operators. The right hand side is basically conjunctive normal form which is useful in proofs. (Contributed by RP, 16-Apr-2020.)

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

**Proof of Theorem ifpim123g**
Step	Hyp	Ref	Expression
1		dfifp4 1016	. . 3 if- $\/$ $/\$ $\/$
2		dfifp4 1016	. . 3 if- $\/$ $/\$ $\/$
3	1, 2	imbi12i 340	. 2 if- if- $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
4		imor 428	. 2 $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$
5		ordi 908	. . 3 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $\/$
6		orass 546	. . . . 5 $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $\/$
7		ianor 509	. . . . . . . . . 10 $\/$ $/\$ $\/$ $\/$ $\/$ $\/$
8		pm4.52 512	. . . . . . . . . . . 12 $/\$ $\/$
9	8	bicomi 214	. . . . . . . . . . 11 $\/$ $/\$
10		ioran 511	. . . . . . . . . . 11 $\/$ $/\$
11	9, 10	orbi12i 543	. . . . . . . . . 10 $\/$ $\/$ $\/$ $/\$ $\/$ $/\$
12		cases2 993	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$
13		imor 428	. . . . . . . . . . . 12 $\/$
14		pm4.66 436	. . . . . . . . . . . 12 $\/$
15	13, 14	anbi12i 733	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $\/$
16	12, 15	bitri 264	. . . . . . . . . 10 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
17	7, 11, 16	3bitri 286	. . . . . . . . 9 $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
18	17	orbi1i 542	. . . . . . . 8 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$
19		orcom 402	. . . . . . . . 9 $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$
20		ordi 908	. . . . . . . . 9 $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$
21	19, 20	bitri 264	. . . . . . . 8 $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$
22		orass 546	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$
23		orcom 402	. . . . . . . . . . . 12 $\/$ $\/$
24		imor 428	. . . . . . . . . . . 12 $\/$
25	23, 24	bitr4i 267	. . . . . . . . . . 11 $\/$
26	25	orbi1i 542	. . . . . . . . . 10 $\/$ $\/$ $\/$
27	22, 26	bitr3i 266	. . . . . . . . 9 $\/$ $\/$ $\/$
28		orass 546	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$
29		imor 428	. . . . . . . . . . . 12 $\/$
30	29	bicomi 214	. . . . . . . . . . 11 $\/$
31	30	orbi1i 542	. . . . . . . . . 10 $\/$ $\/$ $\/$
32	28, 31	bitr3i 266	. . . . . . . . 9 $\/$ $\/$ $\/$
33	27, 32	anbi12i 733	. . . . . . . 8 $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$
34	18, 21, 33	3bitri 286	. . . . . . 7 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$
35	34	orbi1i 542	. . . . . 6 $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$
36		ordir 909	. . . . . 6 $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$
37		orass 546	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
38		imor 428	. . . . . . . . . 10 $\/$
39	38	bicomi 214	. . . . . . . . 9 $\/$
40	39	orbi2i 541	. . . . . . . 8 $\/$ $\/$ $\/$
41	37, 40	bitri 264	. . . . . . 7 $\/$ $\/$ $\/$
42		orass 546	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
43		imor 428	. . . . . . . . . 10 $\/$
44	43	bicomi 214	. . . . . . . . 9 $\/$
45	44	orbi2i 541	. . . . . . . 8 $\/$ $\/$ $\/$
46	42, 45	bitri 264	. . . . . . 7 $\/$ $\/$ $\/$
47	41, 46	anbi12i 733	. . . . . 6 $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$
48	35, 36, 47	3bitri 286	. . . . 5 $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$
49	6, 48	bitr3i 266	. . . 4 $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$
50		orass 546	. . . . 5 $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $\/$
51	17	orbi1i 542	. . . . . . . 8 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$
52		orcom 402	. . . . . . . . 9 $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$
53		ordi 908	. . . . . . . . 9 $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$
54	52, 53	bitri 264	. . . . . . . 8 $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$
55		orass 546	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$
56		orcom 402	. . . . . . . . . . . 12 $\/$ $\/$
57		imor 428	. . . . . . . . . . . 12 $\/$
58	56, 57	bitr4i 267	. . . . . . . . . . 11 $\/$
59	58	orbi1i 542	. . . . . . . . . 10 $\/$ $\/$ $\/$
60	55, 59	bitr3i 266	. . . . . . . . 9 $\/$ $\/$ $\/$
61		orass 546	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$
62		df-or 385	. . . . . . . . . . 11 $\/$
63	62	orbi1i 542	. . . . . . . . . 10 $\/$ $\/$ $\/$
64	61, 63	bitr3i 266	. . . . . . . . 9 $\/$ $\/$ $\/$
65	60, 64	anbi12i 733	. . . . . . . 8 $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$
66	51, 54, 65	3bitri 286	. . . . . . 7 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$
67	66	orbi1i 542	. . . . . 6 $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$
68		ordir 909	. . . . . 6 $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$
69		orass 546	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
70		imor 428	. . . . . . . . . 10 $\/$
71	70	bicomi 214	. . . . . . . . 9 $\/$
72	71	orbi2i 541	. . . . . . . 8 $\/$ $\/$ $\/$
73	69, 72	bitri 264	. . . . . . 7 $\/$ $\/$ $\/$
74		orass 546	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
75		imor 428	. . . . . . . . . 10 $\/$
76	75	bicomi 214	. . . . . . . . 9 $\/$
77	76	orbi2i 541	. . . . . . . 8 $\/$ $\/$ $\/$
78	74, 77	bitri 264	. . . . . . 7 $\/$ $\/$ $\/$
79	73, 78	anbi12i 733	. . . . . 6 $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$
80	67, 68, 79	3bitri 286	. . . . 5 $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$
81	50, 80	bitr3i 266	. . . 4 $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$
82	49, 81	anbi12i 733	. . 3 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
83	5, 82	bitri 264	. 2 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
84	3, 4, 83	3bitri 286	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: ifpim1g 37846 ifpbi1b 37848 ifpimimb 37849 ifpor123g 37853 ifpimim 37854

W3C validator