Theorem ifpim123g 39864

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 1061	. . 3 ⊢ (if-(𝜑, 𝜒, 𝜏) ↔ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)))
2		dfifp4 1061	. . 3 ⊢ (if-(𝜓, 𝜃, 𝜂) ↔ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂)))
3	1, 2	imbi12i 353	. 2 ⊢ ((if-(𝜑, 𝜒, 𝜏) → if-(𝜓, 𝜃, 𝜂)) ↔ (((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) → ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂))))
4		imor 849	. 2 ⊢ ((((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) → ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂))) ↔ (¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂))))
5		ordi 1002	. . 3 ⊢ ((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂))) ↔ ((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ (¬ 𝜓 ∨ 𝜃)) ∧ (¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ (𝜓 ∨ 𝜂))))
6		orass 918	. . . . 5 ⊢ (((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ ¬ 𝜓) ∨ 𝜃) ↔ (¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ (¬ 𝜓 ∨ 𝜃)))
7		ianor 978	. . . . . . . . . 10 ⊢ (¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ↔ (¬ (¬ 𝜑 ∨ 𝜒) ∨ ¬ (𝜑 ∨ 𝜏)))
8		pm4.52 981	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝜒) ↔ ¬ (¬ 𝜑 ∨ 𝜒))
9	8	bicomi 226	. . . . . . . . . . 11 ⊢ (¬ (¬ 𝜑 ∨ 𝜒) ↔ (𝜑 ∧ ¬ 𝜒))
10		ioran 980	. . . . . . . . . . 11 ⊢ (¬ (𝜑 ∨ 𝜏) ↔ (¬ 𝜑 ∧ ¬ 𝜏))
11	9, 10	orbi12i 911	. . . . . . . . . 10 ⊢ ((¬ (¬ 𝜑 ∨ 𝜒) ∨ ¬ (𝜑 ∨ 𝜏)) ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (¬ 𝜑 ∧ ¬ 𝜏)))
12		cases2 1042	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝜒) ∨ (¬ 𝜑 ∧ ¬ 𝜏)) ↔ ((𝜑 → ¬ 𝜒) ∧ (¬ 𝜑 → ¬ 𝜏)))
13		imor 849	. . . . . . . . . . . 12 ⊢ ((𝜑 → ¬ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜒))
14		pm4.66 846	. . . . . . . . . . . 12 ⊢ ((¬ 𝜑 → ¬ 𝜏) ↔ (𝜑 ∨ ¬ 𝜏))
15	13, 14	anbi12i 628	. . . . . . . . . . 11 ⊢ (((𝜑 → ¬ 𝜒) ∧ (¬ 𝜑 → ¬ 𝜏)) ↔ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)))
16	12, 15	bitri 277	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝜒) ∨ (¬ 𝜑 ∧ ¬ 𝜏)) ↔ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)))
17	7, 11, 16	3bitri 299	. . . . . . . . 9 ⊢ (¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ↔ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)))
18	17	orbi1i 910	. . . . . . . 8 ⊢ ((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ ¬ 𝜓) ↔ (((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ ¬ 𝜓))
19		orcom 866	. . . . . . . . 9 ⊢ ((((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ ¬ 𝜓) ↔ (¬ 𝜓 ∨ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏))))
20		ordi 1002	. . . . . . . . 9 ⊢ ((¬ 𝜓 ∨ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏))) ↔ ((¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏))))
21	19, 20	bitri 277	. . . . . . . 8 ⊢ ((((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ ¬ 𝜓) ↔ ((¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏))))
22		orass 918	. . . . . . . . . 10 ⊢ (((¬ 𝜓 ∨ ¬ 𝜑) ∨ ¬ 𝜒) ↔ (¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)))
23		orcom 866	. . . . . . . . . . . 12 ⊢ ((¬ 𝜓 ∨ ¬ 𝜑) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
24		imor 849	. . . . . . . . . . . 12 ⊢ ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
25	23, 24	bitr4i 280	. . . . . . . . . . 11 ⊢ ((¬ 𝜓 ∨ ¬ 𝜑) ↔ (𝜑 → ¬ 𝜓))
26	25	orbi1i 910	. . . . . . . . . 10 ⊢ (((¬ 𝜓 ∨ ¬ 𝜑) ∨ ¬ 𝜒) ↔ ((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒))
27	22, 26	bitr3i 279	. . . . . . . . 9 ⊢ ((¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ↔ ((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒))
28		orass 918	. . . . . . . . . 10 ⊢ (((¬ 𝜓 ∨ 𝜑) ∨ ¬ 𝜏) ↔ (¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏)))
29		imor 849	. . . . . . . . . . . 12 ⊢ ((𝜓 → 𝜑) ↔ (¬ 𝜓 ∨ 𝜑))
30	29	bicomi 226	. . . . . . . . . . 11 ⊢ ((¬ 𝜓 ∨ 𝜑) ↔ (𝜓 → 𝜑))
31	30	orbi1i 910	. . . . . . . . . 10 ⊢ (((¬ 𝜓 ∨ 𝜑) ∨ ¬ 𝜏) ↔ ((𝜓 → 𝜑) ∨ ¬ 𝜏))
32	28, 31	bitr3i 279	. . . . . . . . 9 ⊢ ((¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏)) ↔ ((𝜓 → 𝜑) ∨ ¬ 𝜏))
33	27, 32	anbi12i 628	. . . . . . . 8 ⊢ (((¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏))) ↔ (((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∧ ((𝜓 → 𝜑) ∨ ¬ 𝜏)))
34	18, 21, 33	3bitri 299	. . . . . . 7 ⊢ ((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ ¬ 𝜓) ↔ (((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∧ ((𝜓 → 𝜑) ∨ ¬ 𝜏)))
35	34	orbi1i 910	. . . . . 6 ⊢ (((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ ¬ 𝜓) ∨ 𝜃) ↔ ((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∧ ((𝜓 → 𝜑) ∨ ¬ 𝜏)) ∨ 𝜃))
36		ordir 1003	. . . . . 6 ⊢ (((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∧ ((𝜓 → 𝜑) ∨ ¬ 𝜏)) ∨ 𝜃) ↔ ((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∨ 𝜃) ∧ (((𝜓 → 𝜑) ∨ ¬ 𝜏) ∨ 𝜃)))
37		orass 918	. . . . . . . 8 ⊢ ((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∨ 𝜃) ↔ ((𝜑 → ¬ 𝜓) ∨ (¬ 𝜒 ∨ 𝜃)))
38		imor 849	. . . . . . . . . 10 ⊢ ((𝜒 → 𝜃) ↔ (¬ 𝜒 ∨ 𝜃))
39	38	bicomi 226	. . . . . . . . 9 ⊢ ((¬ 𝜒 ∨ 𝜃) ↔ (𝜒 → 𝜃))
40	39	orbi2i 909	. . . . . . . 8 ⊢ (((𝜑 → ¬ 𝜓) ∨ (¬ 𝜒 ∨ 𝜃)) ↔ ((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)))
41	37, 40	bitri 277	. . . . . . 7 ⊢ ((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∨ 𝜃) ↔ ((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)))
42		orass 918	. . . . . . . 8 ⊢ ((((𝜓 → 𝜑) ∨ ¬ 𝜏) ∨ 𝜃) ↔ ((𝜓 → 𝜑) ∨ (¬ 𝜏 ∨ 𝜃)))
43		imor 849	. . . . . . . . . 10 ⊢ ((𝜏 → 𝜃) ↔ (¬ 𝜏 ∨ 𝜃))
44	43	bicomi 226	. . . . . . . . 9 ⊢ ((¬ 𝜏 ∨ 𝜃) ↔ (𝜏 → 𝜃))
45	44	orbi2i 909	. . . . . . . 8 ⊢ (((𝜓 → 𝜑) ∨ (¬ 𝜏 ∨ 𝜃)) ↔ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃)))
46	42, 45	bitri 277	. . . . . . 7 ⊢ ((((𝜓 → 𝜑) ∨ ¬ 𝜏) ∨ 𝜃) ↔ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃)))
47	41, 46	anbi12i 628	. . . . . 6 ⊢ (((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∨ 𝜃) ∧ (((𝜓 → 𝜑) ∨ ¬ 𝜏) ∨ 𝜃)) ↔ (((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃))))
48	35, 36, 47	3bitri 299	. . . . 5 ⊢ (((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ ¬ 𝜓) ∨ 𝜃) ↔ (((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃))))
49	6, 48	bitr3i 279	. . . 4 ⊢ ((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ (¬ 𝜓 ∨ 𝜃)) ↔ (((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃))))
50		orass 918	. . . . 5 ⊢ (((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ 𝜓) ∨ 𝜂) ↔ (¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ (𝜓 ∨ 𝜂)))
51	17	orbi1i 910	. . . . . . . 8 ⊢ ((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ 𝜓) ↔ (((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ 𝜓))
52		orcom 866	. . . . . . . . 9 ⊢ ((((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ 𝜓) ↔ (𝜓 ∨ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏))))
53		ordi 1002	. . . . . . . . 9 ⊢ ((𝜓 ∨ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏))) ↔ ((𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (𝜓 ∨ (𝜑 ∨ ¬ 𝜏))))
54	52, 53	bitri 277	. . . . . . . 8 ⊢ ((((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ 𝜓) ↔ ((𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (𝜓 ∨ (𝜑 ∨ ¬ 𝜏))))
55		orass 918	. . . . . . . . . 10 ⊢ (((𝜓 ∨ ¬ 𝜑) ∨ ¬ 𝜒) ↔ (𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)))
56		orcom 866	. . . . . . . . . . . 12 ⊢ ((𝜓 ∨ ¬ 𝜑) ↔ (¬ 𝜑 ∨ 𝜓))
57		imor 849	. . . . . . . . . . . 12 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))
58	56, 57	bitr4i 280	. . . . . . . . . . 11 ⊢ ((𝜓 ∨ ¬ 𝜑) ↔ (𝜑 → 𝜓))
59	58	orbi1i 910	. . . . . . . . . 10 ⊢ (((𝜓 ∨ ¬ 𝜑) ∨ ¬ 𝜒) ↔ ((𝜑 → 𝜓) ∨ ¬ 𝜒))
60	55, 59	bitr3i 279	. . . . . . . . 9 ⊢ ((𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ↔ ((𝜑 → 𝜓) ∨ ¬ 𝜒))
61		orass 918	. . . . . . . . . 10 ⊢ (((𝜓 ∨ 𝜑) ∨ ¬ 𝜏) ↔ (𝜓 ∨ (𝜑 ∨ ¬ 𝜏)))
62		df-or 844	. . . . . . . . . . 11 ⊢ ((𝜓 ∨ 𝜑) ↔ (¬ 𝜓 → 𝜑))
63	62	orbi1i 910	. . . . . . . . . 10 ⊢ (((𝜓 ∨ 𝜑) ∨ ¬ 𝜏) ↔ ((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏))
64	61, 63	bitr3i 279	. . . . . . . . 9 ⊢ ((𝜓 ∨ (𝜑 ∨ ¬ 𝜏)) ↔ ((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏))
65	60, 64	anbi12i 628	. . . . . . . 8 ⊢ (((𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (𝜓 ∨ (𝜑 ∨ ¬ 𝜏))) ↔ (((𝜑 → 𝜓) ∨ ¬ 𝜒) ∧ ((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏)))
66	51, 54, 65	3bitri 299	. . . . . . 7 ⊢ ((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ 𝜓) ↔ (((𝜑 → 𝜓) ∨ ¬ 𝜒) ∧ ((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏)))
67	66	orbi1i 910	. . . . . 6 ⊢ (((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ 𝜓) ∨ 𝜂) ↔ ((((𝜑 → 𝜓) ∨ ¬ 𝜒) ∧ ((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏)) ∨ 𝜂))
68		ordir 1003	. . . . . 6 ⊢ (((((𝜑 → 𝜓) ∨ ¬ 𝜒) ∧ ((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏)) ∨ 𝜂) ↔ ((((𝜑 → 𝜓) ∨ ¬ 𝜒) ∨ 𝜂) ∧ (((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏) ∨ 𝜂)))
69		orass 918	. . . . . . . 8 ⊢ ((((𝜑 → 𝜓) ∨ ¬ 𝜒) ∨ 𝜂) ↔ ((𝜑 → 𝜓) ∨ (¬ 𝜒 ∨ 𝜂)))
70		imor 849	. . . . . . . . . 10 ⊢ ((𝜒 → 𝜂) ↔ (¬ 𝜒 ∨ 𝜂))
71	70	bicomi 226	. . . . . . . . 9 ⊢ ((¬ 𝜒 ∨ 𝜂) ↔ (𝜒 → 𝜂))
72	71	orbi2i 909	. . . . . . . 8 ⊢ (((𝜑 → 𝜓) ∨ (¬ 𝜒 ∨ 𝜂)) ↔ ((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)))
73	69, 72	bitri 277	. . . . . . 7 ⊢ ((((𝜑 → 𝜓) ∨ ¬ 𝜒) ∨ 𝜂) ↔ ((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)))
74		orass 918	. . . . . . . 8 ⊢ ((((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏) ∨ 𝜂) ↔ ((¬ 𝜓 → 𝜑) ∨ (¬ 𝜏 ∨ 𝜂)))
75		imor 849	. . . . . . . . . 10 ⊢ ((𝜏 → 𝜂) ↔ (¬ 𝜏 ∨ 𝜂))
76	75	bicomi 226	. . . . . . . . 9 ⊢ ((¬ 𝜏 ∨ 𝜂) ↔ (𝜏 → 𝜂))
77	76	orbi2i 909	. . . . . . . 8 ⊢ (((¬ 𝜓 → 𝜑) ∨ (¬ 𝜏 ∨ 𝜂)) ↔ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂)))
78	74, 77	bitri 277	. . . . . . 7 ⊢ ((((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏) ∨ 𝜂) ↔ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂)))
79	73, 78	anbi12i 628	. . . . . 6 ⊢ (((((𝜑 → 𝜓) ∨ ¬ 𝜒) ∨ 𝜂) ∧ (((¬ 𝜓 → 𝜑) ∨ ¬ 𝜏) ∨ 𝜂)) ↔ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂))))
80	67, 68, 79	3bitri 299	. . . . 5 ⊢ (((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ 𝜓) ∨ 𝜂) ↔ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂))))
81	50, 80	bitr3i 279	. . . 4 ⊢ ((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ (𝜓 ∨ 𝜂)) ↔ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂))))
82	49, 81	anbi12i 628	. . 3 ⊢ (((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ (¬ 𝜓 ∨ 𝜃)) ∧ (¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ (𝜓 ∨ 𝜂))) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂)))))
83	5, 82	bitri 277	. 2 ⊢ ((¬ ((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∨ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂))) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂)))))
84	3, 4, 83	3bitri 299	1 ⊢ ((if-(𝜑, 𝜒, 𝜏) → if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843  if-wif 1057

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 209  df-an 399  df-or 844  df-ifp 1058

This theorem is referenced by:  ifpim1g  39865  ifpbi1b  39867  ifpimimb  39868  ifpor123g  39872  ifpimim  39873